Showing error 26

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

Source: 

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