Showing error 2197

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


Source:

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)
1034{
1035  pthread_t id1, id2;
1036  enqueue_flag=(1);
1037  dequeue_flag=(0);
1038  init(&queue);
1039  if (!empty(&queue)==(-1)) {
1040    goto ERROR;
1041    ERROR:
1042      ;
1043  }
1044  pthread_mutex_init(&m, 0);
1045  pthread_create(&id1, ((void *)0), t1, &queue);
1046  pthread_create(&id2, ((void *)0), t2, &queue);
1047  pthread_join(id1, ((void *)0));
1048  pthread_join(id2, ((void *)0));
1049  return 0;
1050}
Show full sources