Showing error 2013

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


Source:

 176#line 85
 177  tmp = valid_product();
 178  }
 179#line 85
 180  if (tmp) {
 181    {
 182#line 86
 183    setup();
 184#line 87
 185    runTest();
 186    }
 187  } else {
 188
 189  }
 190#line 1226 "Test.c"
 191  retValue_acc = 0;
 192#line 1228
 193  return (retValue_acc);
 194#line 1235
 195  return (retValue_acc);
 196}
 197}
 198#line 1 "wsllib_check.o"
 199#pragma merger(0,"wsllib_check.i","")
 200#line 3 "wsllib_check.c"
 201void __automaton_fail(void) 
 202{ 
 203
 204  {
 205  goto ERROR;
 206  ERROR: ;
 207#line 53 "wsllib_check.c"
 208  return;
 209}
 210}
 211#line 1 "Specification3_spec.o"
 212#pragma merger(0,"Specification3_spec.i","")
 213#line 10 "MinePump.h"
 214int isPumpRunning(void) ;
 215#line 10 "Environment.h"
 216int isMethaneLevelCritical(void) ;
Show full sources