Showing error 25

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

Source: 

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