Showing error 1940

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

Source: 

1003#line 20 "featureselect.c"
1004void select_helpers(void) 
1005{ 
1006
1007  {
1008#line 111 "featureselect.c"
1009  return;
1010}
1011}
1012#line 25 "featureselect.c"
1013int valid_product(void) 
1014{ int retValue_acc ;
1015
1016  {
1017#line 129 "featureselect.c"
1018  retValue_acc = 1;
1019#line 131
1020  return (retValue_acc);
1021#line 138
1022  return (retValue_acc);
1023}
1024}
1025#line 1 "wsllib_check.o"
1026#pragma merger(0,"wsllib_check.i","")
1027#line 3 "wsllib_check.c"
1028void __automaton_fail(void) 
1029{ 
1030
1031  {
1032  goto ERROR;
1033  ERROR: ;
1034#line 53 "wsllib_check.c"
1035  return;
1036}
1037}
1038#line 1 "Test.o"
1039#pragma merger(0,"Test.i","")
1040#line 8 "Test.c"
1041int cleanupTimeShifts  =    4;
1042#line 11 "Test.c"
1043#line 17 "Test.c"
Show full sources
↑