Showing error 11

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: pthread/twostage_3_BUG.cil.c
Line in file: 218
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

188    }
189#line 37
190    return ((void *)0);
191  } else {
192
193  }
194  {
195#line 39
196  t1 = data1Value;
197#line 40
198  pthread_mutex_unlock(data1Lock);
199#line 42
200  pthread_mutex_lock(data2Lock);
201#line 43
202  t2 = data2Value;
203#line 44
204  pthread_mutex_unlock(data2Lock);
205  }
206  {
207#line 46
208  __cil_tmp4 = t1 + 1;
209#line 46
210  if (t2 != __cil_tmp4) {
211    {
212#line 47
213    __cil_tmp5 = (FILE * __restrict  )stderr;
214#line 47
215    __cil_tmp6 = (char const   * __restrict  )"Bug found!\n";
216#line 47
217    fprintf(__cil_tmp5, __cil_tmp6);
218    ERROR: goto ERROR;
219    }
220
221  } else {
222
223  }
224  }
225#line 52
226  return ((void *)0);
227}
228}
Show full sources