Showing error 2196

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_ok_safe.i
Line in file: 1023
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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