Showing error 2211

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


Source:

2041
2042  while (num == 0)
2043    pthread_cond_wait(&full, &m);
2044
2045  num--;
2046
2047  pthread_mutex_unlock(&m);
2048
2049  pthread_cond_signal(&empty);
2050}
2051
2052
2053int main()
2054{
2055  pthread_t t1, t2;
2056
2057  num = 1;
2058
2059  pthread_mutex_init(&m, 0);
2060  pthread_cond_init(&empty, 0);
2061  pthread_cond_init(&full, 0);
2062
2063  pthread_create(&t1, 0, thread1, 0);
2064  pthread_create(&t2, 0, thread2, 0);
2065
2066  pthread_join(t1, 0);
2067  pthread_join(t2, 0);
2068
2069  if (num!=1)
2070  {
2071    ERROR: goto ERROR;
2072    ;
2073  }
2074
2075  return 0;
2076
2077}
Show full sources