Showing error 24

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

Source: 

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