Showing error 31

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

Source: 

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