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_spec3_product30_unsafe.cil.c |
Line in file: | 1241 |
Project: | SV-COMP 2013 |
Project version: | 2.6.28 |
Tools: |
Manual Work
|
Entered: | 2013-01-17 16:57:54 UTC |
1211#line 355 1212 tmp___0 = 1; 1213 } 1214#line 355 1215 retValue_acc = tmp___0; 1216#line 357 1217 return (retValue_acc); 1218#line 364 1219 return (retValue_acc); 1220} 1221} 1222#line 84 "MinePump.c" 1223void startSystem(void) 1224{ 1225 1226 { 1227#line 86 1228 systemActive = 1; 1229#line 388 "MinePump.c" 1230 return; 1231} 1232} 1233#line 1 "wsllib_check.o" 1234#pragma merger(0,"wsllib_check.i","") 1235#line 3 "wsllib_check.c" 1236void __automaton_fail(void) 1237{ 1238 1239 { 1240 goto ERROR; 1241 ERROR: ; 1242#line 53 "wsllib_check.c" 1243 return; 1244} 1245} 1246#line 1 "featureselect.o" 1247#pragma merger(0,"featureselect.i","") 1248#line 8 "featureselect.h" 1249int select_one(void) ; 1250#line 8 "featureselect.c" 1251int select_one(void)