Showing error 2201

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

Source: 

 991    q->head++;
 992  return x;
 993}
 994void *t1(void *arg)
 995{
 996  int value, i;
 997  pthread_mutex_lock(&m);
 998  value = nondet_int();
 999  if (enqueue(&queue,value)) {
1000    goto ERROR;
1001  }
1002  stored_elements[0]=value;
1003  if (empty(&queue)) {
1004    goto ERROR;
1005  }
1006  pthread_mutex_unlock(&m);
1007  for(i=0; i<((20)-1); i++)
1008  {
1009    pthread_mutex_lock(&m);
1010    if (enqueue_flag)
1011    {
1012      value = nondet_int();
1013      enqueue(&queue,value);
1014      stored_elements[i+1]=value;
1015      enqueue_flag=(0);
1016      dequeue_flag=(1);
1017    }
1018    pthread_mutex_unlock(&m);
1019  }
1020  return ((void *)0);
1021  ERROR:
1022    ;
1023}
1024void *t2(void *arg)
1025{
1026  int i;
1027  for(i=0; i<(20); i++)
1028  {
1029    pthread_mutex_lock(&m);
1030    if (dequeue_flag)
1031    {
Show full sources
↑