Showing error 1618

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


Source:

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