Showing error 2200

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


Source:

557  pthread_t __cil_tmp15 ;
558  void *__cil_tmp16 ;
559  void **__cil_tmp17 ;
560  pthread_t *__cil_tmp18 ;
561  pthread_t __cil_tmp19 ;
562  void *__cil_tmp20 ;
563  void **__cil_tmp21 ;
564
565  {
566  {
567#line 149
568  enqueue_flag = (_Bool)1;
569#line 150
570  dequeue_flag = (_Bool)0;
571#line 152
572  init(& queue);
573#line 154
574  tmp = empty(& queue);
575  }
576#line 154
577  if (tmp) {
578#line 154
579    tmp___0 = 0;
580  } else {
581#line 154
582    tmp___0 = 1;
583  }
584#line 154
585  if (tmp___0 == -1) {
586    goto ERROR;
587    ERROR: ;
588  } else {
589
590  }
591  {
592#line 161
593  __cil_tmp5 = (pthread_mutexattr_t const   *)0;
594#line 161
595  pthread_mutex_init(& m, __cil_tmp5);
596#line 163
597  __cil_tmp6 = (pthread_t * __restrict  )(& id1);
Show full sources