Showing error 1918

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


Source:

 112#line 12
 113      if (tmp___1) {
 114
 115      } else {
 116
 117      }
 118    }
 119    {
 120#line 13
 121    timeShift();
 122    }
 123  }
 124  while_0_break: /* CIL Label */ ;
 125  }
 126  {
 127#line 15
 128  cleanup();
 129  }
 130#line 74 "scenario.c"
 131  return;
 132}
 133}
 134#line 1 "wsllib_check.o"
 135#pragma merger(0,"wsllib_check.i","")
 136#line 3 "wsllib_check.c"
 137void __automaton_fail(void) 
 138{ 
 139
 140  {
 141  goto ERROR;
 142  ERROR: ;
 143#line 53 "wsllib_check.c"
 144  return;
 145}
 146}
 147#line 1 "MinePump.o"
 148#pragma merger(0,"MinePump.i","")
 149#line 4 "Environment.h"
 150void lowerWaterLevel(void) ;
 151#line 10
 152int isMethaneLevelCritical(void) ;
Show full sources