Showing error 1631

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

Source: 

2731#pragma merger(0,"scenario.i","")
2732#line 1 "scenario.c"
2733void test(void) 
2734{ 
2735
2736  {
2737  {
2738#line 2
2739  initTopDown();
2740#line 3
2741  bobCall();
2742#line 4
2743  threeTS();
2744#line 5
2745  bobCall();
2746#line 6
2747  cleanup();
2748  }
2749#line 59 "scenario.c"
2750  return;
2751}
2752}
2753#line 1 "wsllib_check.o"
2754#pragma merger(0,"wsllib_check.i","")
2755#line 3 "wsllib_check.c"
2756void __automaton_fail(void) 
2757{ 
2758
2759  {
2760  goto ERROR;
2761  ERROR: ;
2762#line 53 "wsllib_check.c"
2763  return;
2764}
2765}
2766#line 1 "Elevator.o"
2767#pragma merger(0,"Elevator.i","")
2768#line 359 "/usr/include/stdio.h"
2769extern int printf(char const   * __restrict  __format  , ...) ;
2770#line 16 "Person.h"
2771void enterElevator(int p ) ;
Show full sources
↑