Showing error 1934

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

Source: 

 397#line 12
 398      if (tmp___1) {
 399
 400      } else {
 401
 402      }
 403    }
 404    {
 405#line 13
 406    timeShift();
 407    }
 408  }
 409  while_0_break: /* CIL Label */ ;
 410  }
 411  {
 412#line 15
 413  cleanup();
 414  }
 415#line 74 "scenario.c"
 416  return;
 417}
 418}
 419#line 1 "wsllib_check.o"
 420#pragma merger(0,"wsllib_check.i","")
 421#line 3 "wsllib_check.c"
 422void __automaton_fail(void) 
 423{ 
 424
 425  {
 426  goto ERROR;
 427  ERROR: ;
 428#line 53 "wsllib_check.c"
 429  return;
 430}
 431}
 432#line 1 "Test.o"
 433#pragma merger(0,"Test.i","")
 434#line 8 "Test.c"
 435int cleanupTimeShifts  =    4;
 436#line 11 "Test.c"
 437#line 17 "Test.c"
Show full sources
↑