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_product42_unsafe.cil.c |
Line in file: | 1190 |
Project: | SV-COMP 2013 |
Project version: | 2.6.28 |
Tools: |
Manual Work
|
Entered: | 2013-01-17 16:57:54 UTC |
1160#line 85 1161 tmp = valid_product(); 1162 } 1163#line 85 1164 if (tmp) { 1165 { 1166#line 86 1167 setup(); 1168#line 87 1169 runTest(); 1170 } 1171 } else { 1172 1173 } 1174#line 1234 "Test.c" 1175 retValue_acc = 0; 1176#line 1236 1177 return (retValue_acc); 1178#line 1243 1179 return (retValue_acc); 1180} 1181} 1182#line 1 "wsllib_check.o" 1183#pragma merger(0,"wsllib_check.i","") 1184#line 3 "wsllib_check.c" 1185void __automaton_fail(void) 1186{ 1187 1188 { 1189 goto ERROR; 1190 ERROR: ; 1191#line 53 "wsllib_check.c" 1192 return; 1193} 1194} 1195#line 1 "Environment.o" 1196#pragma merger(0,"Environment.i","") 1197#line 12 "Environment.h" 1198int getWaterLevel(void) ; 1199#line 9 "Environment.c" 1200int waterLevel = 1;