Showing error 1615

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

Source: 

2569#line 412
2570          i___0 = i___0 + 1;
2571        }
2572        while_4_break: /* CIL Label */ ;
2573        }
2574#line 412
2575        i___0 = i___0 - 1;
2576      }
2577      while_3_break: /* CIL Label */ ;
2578      }
2579    } else {
2580
2581    }
2582  }
2583#line 2464 "Elevator.c"
2584  retValue_acc = 0;
2585#line 2466
2586  return (retValue_acc);
2587#line 2473
2588  return (retValue_acc);
2589}
2590}
2591#line 1 "wsllib_check.o"
2592#pragma merger(0,"wsllib_check.i","")
2593#line 3 "wsllib_check.c"
2594void __automaton_fail(void) 
2595{ 
2596
2597  {
2598  goto ERROR;
2599  ERROR: ;
2600#line 53 "wsllib_check.c"
2601  return;
2602}
2603}
2604#line 1 "libacc.o"
2605#pragma merger(0,"libacc.i","")
2606#line 73 "/usr/include/assert.h"
2607extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
2608                                                                      char const   *__file ,
2609                                                                      unsigned int __line ,
Show full sources
↑