Showing error 1629

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

Source: 

2739#line 176
2740  tmp = valid_product();
2741  }
2742#line 176
2743  if (tmp) {
2744    {
2745#line 177
2746    setup();
2747#line 178
2748    runTest();
2749    }
2750  } else {
2751
2752  }
2753#line 1620 "Test.c"
2754  retValue_acc = 0;
2755#line 1622
2756  return (retValue_acc);
2757#line 1629
2758  return (retValue_acc);
2759}
2760}
2761#line 1 "wsllib_check.o"
2762#pragma merger(0,"wsllib_check.i","")
2763#line 3 "wsllib_check.c"
2764void __automaton_fail(void) 
2765{ 
2766
2767  {
2768  goto ERROR;
2769  ERROR: ;
2770#line 53 "wsllib_check.c"
2771  return;
2772}
2773}
2774#line 1 "Elevator.o"
2775#pragma merger(0,"Elevator.i","")
2776#line 359 "/usr/include/stdio.h"
2777extern int printf(char const   * __restrict  __format  , ...) ;
2778#line 16 "Person.h"
2779void enterElevator(int p ) ;
Show full sources
↑