Showing error 2193

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

Source: 

1313extern void __assert (const char *__assertion, const char *__file, int __line)
1314     __attribute__ ((__nothrow__)) __attribute__ ((__noreturn__));
1315
1316
1317
1318# 3 "lazy01_bad.c" 2
1319
1320pthread_mutex_t mutex;
1321int data = 0;
1322
1323void *thread1(void *arg)
1324{
1325  pthread_mutex_lock(&mutex);
1326  data++;
1327  pthread_mutex_unlock(&mutex);
1328}
1329
1330
1331void *thread2(void *arg)
1332{
1333  pthread_mutex_lock(&mutex);
1334  data+=2;
1335  pthread_mutex_unlock(&mutex);
1336}
1337
1338
1339void *thread3(void *arg)
1340{
1341  pthread_mutex_lock(&mutex);
1342  if (data >= 3){
1343    ERROR: goto ERROR;
1344    ;
1345  }
1346  pthread_mutex_unlock(&mutex);
1347}
1348
1349
1350int main()
1351{
1352  pthread_mutex_init(&mutex, 0);
1353
Show full sources
↑