Showing error 1909

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


Source:

1041    deactivatePump();
1042    }
1043  } else {
1044
1045  }
1046#line 64
1047  systemActive = 0;
1048#line 286 "MinePump.c"
1049  return;
1050}
1051}
1052#line 66 "MinePump.c"
1053void startSystem(void) 
1054{ 
1055
1056  {
1057#line 68
1058  systemActive = 1;
1059#line 306 "MinePump.c"
1060  return;
1061}
1062}
1063#line 1 "wsllib_check.o"
1064#pragma merger(0,"wsllib_check.i","")
1065#line 3 "wsllib_check.c"
1066void __automaton_fail(void) 
1067{ 
1068
1069  {
1070  goto ERROR;
1071  ERROR: ;
1072#line 53 "wsllib_check.c"
1073  return;
1074}
1075}
1076#line 1 "Environment.o"
1077#pragma merger(0,"Environment.i","")
1078#line 12 "Environment.h"
1079int getWaterLevel(void) ;
1080#line 9 "Environment.c"
1081int waterLevel  =    1;
Show full sources