Showing error 1648

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

Source: 

1133#pragma merger(0,"scenario.i","")
1134#line 1 "scenario.c"
1135void test(void) 
1136{ 
1137
1138  {
1139  {
1140#line 2
1141  initTopDown();
1142#line 3
1143  bobCall();
1144#line 4
1145  threeTS();
1146#line 5
1147  bobCall();
1148#line 6
1149  cleanup();
1150  }
1151#line 59 "scenario.c"
1152  return;
1153}
1154}
1155#line 1 "wsllib_check.o"
1156#pragma merger(0,"wsllib_check.i","")
1157#line 3 "wsllib_check.c"
1158void __automaton_fail(void) 
1159{ 
1160
1161  {
1162  goto ERROR;
1163  ERROR: ;
1164#line 53 "wsllib_check.c"
1165  return;
1166}
1167}
1168#line 1 "Elevator.o"
1169#pragma merger(0,"Elevator.i","")
1170#line 359 "/usr/include/stdio.h"
1171extern int printf(char const   * __restrict  __format  , ...) ;
1172#line 16 "Person.h"
1173void enterElevator(int p ) ;
Show full sources
↑