Showing error 2202

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: 1034
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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    {
1032      if (!dequeue(&queue)==stored_elements[i]) {
1033        goto ERROR;
1034        ERROR:
1035          ;
1036      }
1037      dequeue_flag=(0);
1038      enqueue_flag=(1);
1039    }
1040    pthread_mutex_unlock(&m);
1041  }
1042  return ((void *)0);
1043}
1044int main(void)
Show full sources
↑