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_safe.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 |
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