Showing error 2209

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


Source:

1311void * thread2(void * arg)
1312{
1313  pthread_mutex_lock(&ma);
1314  data1+=5;
1315  pthread_mutex_unlock(&ma);
1316
1317  pthread_mutex_lock(&ma);
1318  data2-=6;
1319  pthread_mutex_unlock(&ma);
1320}
1321
1322
1323int main()
1324{
1325  pthread_t t1, t2;
1326
1327  pthread_mutex_init(&ma, 0);
1328  pthread_mutex_init(&mb, 0);
1329
1330  data1 = 10;
1331  data2 = 10;
1332
1333  pthread_create(&t1, 0, thread1, 0);
1334  pthread_create(&t2, 0, thread2, 0);
1335
1336  pthread_join(t1, 0);
1337  pthread_join(t2, 0);
1338
1339  if (data1!=16 && data2!=5)
1340  {
1341    ERROR: goto ERROR;
1342      ;
1343  }
1344
1345  return 0;
1346}
Show full sources