Showing error 32

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

Source: 

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