Showing error 1865

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

Source: 

 253#line 17
 254  if (tmp) {
 255    {
 256#line 17
 257    tmp___0 = isPumpRunning();
 258    }
 259#line 17
 260    if (tmp___0) {
 261      {
 262#line 14
 263      __automaton_fail();
 264      }
 265    } else {
 266
 267    }
 268  } else {
 269
 270  }
 271#line 14
 272  return;
 273}
 274}
 275#line 1 "wsllib_check.o"
 276#pragma merger(0,"wsllib_check.i","")
 277#line 3 "wsllib_check.c"
 278void __automaton_fail(void) 
 279{ 
 280
 281  {
 282  goto ERROR;
 283  ERROR: ;
 284#line 53 "wsllib_check.c"
 285  return;
 286}
 287}
 288#line 1 "MinePump.o"
 289#pragma merger(0,"MinePump.i","")
 290#line 4 "MinePump.h"
 291void timeShift(void) ;
 292#line 6
 293void activatePump(void) ;
Show full sources
↑