Showing error 2190

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: pthread/fib_bench_unsafe.cil.c
Line in file: 144
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

  1/* Generated by CIL v. 1.3.7 */
  2/* print_CIL_Input is true */
  3
  4#line 50 "/usr/include/bits/pthreadtypes.h"
  5typedef unsigned long pthread_t;
  6#line 53 "/usr/include/bits/pthreadtypes.h"
  7union __anonunion_pthread_attr_t_3 {
  8   char __size[56] ;
  9   long __align ;
 10};
 11#line 53 "/usr/include/bits/pthreadtypes.h"
 12typedef union __anonunion_pthread_attr_t_3 pthread_attr_t;
 13#line 225 "/usr/include/pthread.h"
 14extern  __attribute__((__nothrow__)) int pthread_create(pthread_t * __restrict  __newthread ,
 15                                                        pthread_attr_t const   * __restrict  __attr ,
 16                                                        void *(*__start_routine)(void * ) ,
 17                                                        void * __restrict  __arg )  __attribute__((__nonnull__(1,3))) ;
 18#line 234
 19extern  __attribute__((__noreturn__)) void pthread_exit(void *__retval ) ;
 20#line 3 "fib_bench_BUG.c"
 21int i  =    1;
 22#line 3 "fib_bench_BUG.c"
 23int j  =    1;
 24#line 7 "fib_bench_BUG.c"
 25void *t1(void *arg ) 
 26{ int k ;
 27  void *__cil_tmp3 ;
 28
 29  {
 30#line 10
 31  k = 0;
 32#line 12
 33  k = 0;
 34  {
 35#line 12
 36  while (1) {
 37    while_0_continue: /* CIL Label */ ;
 38#line 12
 39    if (k < 5) {
 40
 41    } else {
 42      goto while_0_break;
 43    }
 44#line 13
 45    i = i + j;
 46#line 12
 47    k = k + 1;
 48  }
 49  while_0_break: /* CIL Label */ ;
 50  }
 51  {
 52#line 15
 53  __cil_tmp3 = (void *)0;
 54#line 15
 55  pthread_exit(__cil_tmp3);
 56  }
 57}
 58}
 59#line 18 "fib_bench_BUG.c"
 60void *t2(void *arg ) 
 61{ int k ;
 62  void *__cil_tmp3 ;
 63
 64  {
 65#line 21
 66  k = 0;
 67#line 23
 68  k = 0;
 69  {
 70#line 23
 71  while (1) {
 72    while_1_continue: /* CIL Label */ ;
 73#line 23
 74    if (k < 5) {
 75
 76    } else {
 77      goto while_1_break;
 78    }
 79#line 24
 80    j = j + i;
 81#line 23
 82    k = k + 1;
 83  }
 84  while_1_break: /* CIL Label */ ;
 85  }
 86  {
 87#line 26
 88  __cil_tmp3 = (void *)0;
 89#line 26
 90  pthread_exit(__cil_tmp3);
 91  }
 92}
 93}
 94#line 29 "fib_bench_BUG.c"
 95int main(int argc , char **argv ) 
 96{ pthread_t id1 ;
 97  pthread_t id2 ;
 98  pthread_t * __restrict  __cil_tmp5 ;
 99  void *__cil_tmp6 ;
100  pthread_attr_t const   * __restrict  __cil_tmp7 ;
101  void *__cil_tmp8 ;
102  void * __restrict  __cil_tmp9 ;
103  pthread_t * __restrict  __cil_tmp10 ;
104  void *__cil_tmp11 ;
105  pthread_attr_t const   * __restrict  __cil_tmp12 ;
106  void *__cil_tmp13 ;
107  void * __restrict  __cil_tmp14 ;
108
109  {
110  {
111#line 34
112  __cil_tmp5 = (pthread_t * __restrict  )(& id1);
113#line 34
114  __cil_tmp6 = (void *)0;
115#line 34
116  __cil_tmp7 = (pthread_attr_t const   * __restrict  )__cil_tmp6;
117#line 34
118  __cil_tmp8 = (void *)0;
119#line 34
120  __cil_tmp9 = (void * __restrict  )__cil_tmp8;
121#line 34
122  pthread_create(__cil_tmp5, __cil_tmp7, & t1, __cil_tmp9);
123#line 35
124  __cil_tmp10 = (pthread_t * __restrict  )(& id2);
125#line 35
126  __cil_tmp11 = (void *)0;
127#line 35
128  __cil_tmp12 = (pthread_attr_t const   * __restrict  )__cil_tmp11;
129#line 35
130  __cil_tmp13 = (void *)0;
131#line 35
132  __cil_tmp14 = (void * __restrict  )__cil_tmp13;
133#line 35
134  pthread_create(__cil_tmp10, __cil_tmp12, & t2, __cil_tmp14);
135  }
136#line 37
137  if (i >= 144) {
138    goto _L;
139  } else {
140#line 37
141    if (j >= 144) {
142      _L: /* CIL Label */ 
143      goto ERROR;
144      ERROR: ;
145    } else {
146
147    }
148  }
149#line 43
150  return (0);
151}
152}
↑