Showing error 1927

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: product-lines/minepump_spec2_product22_safe.cil.c
Line in file: 1096
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

1066#line 12
1067      if (tmp___1) {
1068
1069      } else {
1070
1071      }
1072    }
1073    {
1074#line 14
1075    timeShift();
1076    }
1077  }
1078  while_4_break: /* CIL Label */ ;
1079  }
1080  {
1081#line 16
1082  cleanup();
1083  }
1084#line 76 "scenario.c"
1085  return;
1086}
1087}
1088#line 1 "wsllib_check.o"
1089#pragma merger(0,"wsllib_check.i","")
1090#line 3 "wsllib_check.c"
1091void __automaton_fail(void) 
1092{ 
1093
1094  {
1095  goto ERROR;
1096  ERROR: ;
1097#line 53 "wsllib_check.c"
1098  return;
1099}
1100}
1101#line 1 "Specification2_spec.o"
1102#pragma merger(0,"Specification2_spec.i","")
1103#line 7 "Specification2_spec.c"
1104int methAndRunningLastTime  ;
1105#line 11 "Specification2_spec.c"
1106void __utac_acc__Specification2_spec__1(void)
Show full sources
↑