Showing error 35

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

Source: 

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