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 |
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;