Showing error 27

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: bitvector/s3_clnt_2_unsafe.BV.c.cil.c
Line in file: 604
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

574        if (cb != 0) {
575          if (s__state != state) {
576            new_state = s__state;
577            s__state = state;
578            s__state = new_state;
579          } else {
580
581          }
582        } else {
583
584        }
585      } else {
586
587      }
588    } else {
589
590    }
591    skip = 0;
592  }
593  while_0_break: /* CIL Label */ ;
594  }
595  end: 
596  s__in_handshake = s__in_handshake - 1;
597  if (cb != 0) {
598
599  } else {
600
601  }
602  __retres59 = ret;
603  goto return_label;
604  ERROR: 
605  {
606  }
607  __retres59 = -1;
608  return_label: /* CIL Label */ 
609  return (__retres59);
610}
611}
612int main(void) 
613{ int __retres1 ;
614
Show full sources
↑