Showing error 1593

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

Source: 

3437#line 176
3438  tmp = valid_product();
3439  }
3440#line 176
3441  if (tmp) {
3442    {
3443#line 177
3444    setup();
3445#line 178
3446    runTest();
3447    }
3448  } else {
3449
3450  }
3451#line 1604 "Test.c"
3452  retValue_acc = 0;
3453#line 1606
3454  return (retValue_acc);
3455#line 1613
3456  return (retValue_acc);
3457}
3458}
3459#line 1 "wsllib_check.o"
3460#pragma merger(0,"wsllib_check.i","")
3461#line 3 "wsllib_check.c"
3462void __automaton_fail(void) 
3463{ 
3464
3465  {
3466  goto ERROR;
3467  ERROR: ;
3468#line 53 "wsllib_check.c"
3469  return;
3470}
3471}
3472#line 1 "UnitTests.o"
3473#pragma merger(0,"UnitTests.i","")
3474#line 24 "UnitTests.c"
3475void spec1(void) 
3476{ int tmp ;
3477  int tmp___0 ;
Show full sources
↑