Showing error 33

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

Source: 

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