Showing error 1870

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


Source:

 887  {
 888#line 209 "Environment.c"
 889  retValue_acc = waterLevel;
 890#line 211
 891  return (retValue_acc);
 892#line 218
 893  return (retValue_acc);
 894}
 895}
 896#line 58 "Environment.c"
 897int isLowWaterSensorDry(void) 
 898{ int retValue_acc ;
 899
 900  {
 901#line 240 "Environment.c"
 902  retValue_acc = waterLevel == 0;
 903#line 242
 904  return (retValue_acc);
 905#line 249
 906  return (retValue_acc);
 907}
 908}
 909#line 1 "wsllib_check.o"
 910#pragma merger(0,"wsllib_check.i","")
 911#line 3 "wsllib_check.c"
 912void __automaton_fail(void) 
 913{ 
 914
 915  {
 916  goto ERROR;
 917  ERROR: ;
 918#line 53 "wsllib_check.c"
 919  return;
 920}
 921}
 922#line 1 "MinePump.o"
 923#pragma merger(0,"MinePump.i","")
 924#line 6 "MinePump.h"
 925void activatePump(void) ;
 926#line 8
 927void deactivatePump(void) ;
Show full sources