Showing error 29

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

Source: 

581        if (cb != 0) {
582          if (s__state != state) {
583            new_state = s__state;
584            s__state = state;
585            s__state = new_state;
586          } else {
587
588          }
589        } else {
590
591        }
592      } else {
593
594      }
595    } else {
596
597    }
598    skip = 0;
599  }
600  while_0_break: /* CIL Label */ ;
601  }
602  end: 
603  s__in_handshake = s__in_handshake - 1;
604  if (cb != 0) {
605
606  } else {
607
608  }
609  __retres60 = ret;
610  goto return_label;
611  ERROR: 
612  {
613  }
614  __retres60 = -1;
615  return_label: /* CIL Label */ 
616  return (__retres60);
617}
618}
619int main(void) 
620{ int __retres1 ;
621
Show full sources
↑