Showing error 34

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

Source: 

633        if (cb != 0) {
634          if (s__state != state) {
635            new_state = s__state;
636            s__state = state;
637            s__state = new_state;
638          } else {
639
640          }
641        } else {
642
643        }
644      } else {
645
646      }
647    } else {
648
649    }
650    skip = 0;
651  }
652  while_0_break: /* CIL Label */ ;
653  }
654  end: 
655  s__in_handshake = s__in_handshake - 1;
656  if (cb != 0) {
657
658  } else {
659
660  }
661  __retres67 = ret;
662  goto return_label;
663  ERROR: 
664  {
665  }
666  __retres67 = -1;
667  return_label: /* CIL Label */ 
668  return (__retres67);
669}
670}
671int main(void) 
672{ int s ;
673  int tmp ;
Show full sources
↑