Showing error 2195

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


Source:

523  pthread_t __cil_tmp15 ;
524  void *__cil_tmp16 ;
525  void **__cil_tmp17 ;
526  pthread_t *__cil_tmp18 ;
527  pthread_t __cil_tmp19 ;
528  void *__cil_tmp20 ;
529  void **__cil_tmp21 ;
530
531  {
532  {
533#line 134
534  enqueue_flag = (_Bool)1;
535#line 135
536  dequeue_flag = (_Bool)0;
537#line 137
538  init(& queue);
539#line 139
540  tmp = empty(& queue);
541  }
542#line 139
543  if (tmp) {
544#line 139
545    tmp___0 = 0;
546  } else {
547#line 139
548    tmp___0 = 1;
549  }
550#line 139
551  if (tmp___0 == -1) {
552    goto ERROR;
553    ERROR: ;
554  } else {
555
556  }
557  {
558#line 145
559  __cil_tmp5 = (pthread_mutexattr_t const   *)0;
560#line 145
561  pthread_mutex_init(& m, __cil_tmp5);
562#line 147
563  __cil_tmp6 = (pthread_t * __restrict  )(& id1);
Show full sources