Showing error 1570

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

Source: 

3166          {
3167#line 57
3168          __automaton_fail();
3169          }
3170        } else {
3171#line 58
3172          if (landingButtons_spc1_4) {
3173            {
3174#line 58
3175            __automaton_fail();
3176            }
3177          } else {
3178
3179          }
3180        }
3181      }
3182    }
3183  }
3184#line 58
3185  return;
3186}
3187}
3188#line 1 "wsllib_check.o"
3189#pragma merger(0,"wsllib_check.i","")
3190#line 3 "wsllib_check.c"
3191void __automaton_fail(void) 
3192{ 
3193
3194  {
3195  goto ERROR;
3196  ERROR: ;
3197#line 53 "wsllib_check.c"
3198  return;
3199}
3200}
3201#line 1 "Floor.o"
3202#pragma merger(0,"Floor.i","")
3203#line 16 "Floor.h"
3204void callOnFloor(int floorID ) ;
3205#line 9 "Floor.c"
3206int calls_0  ;
Show full sources
↑