Showing error 1926

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

Source: 

 899  {
 900#line 209 "Environment.c"
 901  retValue_acc = waterLevel;
 902#line 211
 903  return (retValue_acc);
 904#line 218
 905  return (retValue_acc);
 906}
 907}
 908#line 58 "Environment.c"
 909int isLowWaterSensorDry(void) 
 910{ int retValue_acc ;
 911
 912  {
 913#line 240 "Environment.c"
 914  retValue_acc = waterLevel == 0;
 915#line 242
 916  return (retValue_acc);
 917#line 249
 918  return (retValue_acc);
 919}
 920}
 921#line 1 "wsllib_check.o"
 922#pragma merger(0,"wsllib_check.i","")
 923#line 3 "wsllib_check.c"
 924void __automaton_fail(void) 
 925{ 
 926
 927  {
 928  goto ERROR;
 929  ERROR: ;
 930#line 53 "wsllib_check.c"
 931  return;
 932}
 933}
 934#line 1 "featureselect.o"
 935#pragma merger(0,"featureselect.i","")
 936#line 8 "featureselect.h"
 937int select_one(void) ;
 938#line 8 "featureselect.c"
 939int select_one(void)
Show full sources
↑