Showing error 1609

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


Source:

 224          } else {
 225#line 1201
 226            if (person == 5) {
 227#line 1206
 228              retValue_acc = 3;
 229#line 1208
 230              return (retValue_acc);
 231            } else {
 232#line 1214 "Person.c"
 233              retValue_acc = 0;
 234#line 1216
 235              return (retValue_acc);
 236            }
 237          }
 238        }
 239      }
 240    }
 241  }
 242#line 1223 "Person.c"
 243  return (retValue_acc);
 244}
 245}
 246#line 1 "wsllib_check.o"
 247#pragma merger(0,"wsllib_check.i","")
 248#line 3 "wsllib_check.c"
 249void __automaton_fail(void) 
 250{ 
 251
 252  {
 253  goto ERROR;
 254  ERROR: ;
 255#line 53 "wsllib_check.c"
 256  return;
 257}
 258}
 259#line 1 "Floor.o"
 260#pragma merger(0,"Floor.i","")
 261#line 12 "Floor.h"
 262int isFloorCalling(int floorID ) ;
 263#line 14
 264void resetCallOnFloor(int floorID ) ;
Show full sources