Showing error 1916

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


Source:

 906#line 12
 907        stopSystem();
 908        }
 909      } else {
 910
 911      }
 912    }
 913    {
 914#line 14
 915    timeShift();
 916    }
 917  }
 918  while_3_break: /* CIL Label */ ;
 919  }
 920  {
 921#line 16
 922  cleanup();
 923  }
 924#line 76 "scenario.c"
 925  return;
 926}
 927}
 928#line 1 "wsllib_check.o"
 929#pragma merger(0,"wsllib_check.i","")
 930#line 3 "wsllib_check.c"
 931void __automaton_fail(void) 
 932{ 
 933
 934  {
 935  goto ERROR;
 936  ERROR: ;
 937#line 53 "wsllib_check.c"
 938  return;
 939}
 940}
 941#line 1 "Specification2_spec.o"
 942#pragma merger(0,"Specification2_spec.i","")
 943#line 7 "Specification2_spec.c"
 944int methAndRunningLastTime  ;
 945#line 11 "Specification2_spec.c"
 946__inline void __utac_acc__Specification2_spec__1(void) 
Show full sources