Showing error 2203

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


Source:

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)
1045{
1046  pthread_t id1, id2;
1047  enqueue_flag=(1);
1048  dequeue_flag=(0);
1049  init(&queue);
1050  if (!empty(&queue)==(-1)) {
1051    goto ERROR;
1052    ERROR:
1053      ;
1054  }
1055  pthread_mutex_init(&m, 0);
1056  pthread_create(&id1, ((void *)0), t1, &queue);
1057  pthread_create(&id2, ((void *)0), t2, &queue);
1058  pthread_join(id1, ((void *)0));
1059  pthread_join(id2, ((void *)0));
1060  return 0;
1061}
Show full sources