Showing error 1847

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

Source: 

 183#line 17
 184  if (tmp) {
 185    {
 186#line 17
 187    tmp___0 = isPumpRunning();
 188    }
 189#line 17
 190    if (tmp___0) {
 191      {
 192#line 14
 193      __automaton_fail();
 194      }
 195    } else {
 196
 197    }
 198  } else {
 199
 200  }
 201#line 14
 202  return;
 203}
 204}
 205#line 1 "wsllib_check.o"
 206#pragma merger(0,"wsllib_check.i","")
 207#line 3 "wsllib_check.c"
 208void __automaton_fail(void) 
 209{ 
 210
 211  {
 212  goto ERROR;
 213  ERROR: ;
 214#line 53 "wsllib_check.c"
 215  return;
 216}
 217}
 218#line 1 "MinePump.o"
 219#pragma merger(0,"MinePump.i","")
 220#line 4 "MinePump.h"
 221void timeShift(void) ;
 222#line 6
 223void activatePump(void) ;
Show full sources
↑