Showing error 2073

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


Source:

 320}
 321#line 58 "Environment.c"
 322int isHighWaterSensorDry(void) 
 323{ int retValue_acc ;
 324
 325  {
 326#line 65 "Environment.c"
 327  if (waterLevel < 2) {
 328#line 243
 329    retValue_acc = 1;
 330#line 245
 331    return (retValue_acc);
 332  } else {
 333#line 251 "Environment.c"
 334    retValue_acc = 0;
 335#line 253
 336    return (retValue_acc);
 337  }
 338#line 260 "Environment.c"
 339  return (retValue_acc);
 340}
 341}
 342#line 1 "wsllib_check.o"
 343#pragma merger(0,"wsllib_check.i","")
 344#line 3 "wsllib_check.c"
 345void __automaton_fail(void) 
 346{ 
 347
 348  {
 349  goto ERROR;
 350  ERROR: ;
 351#line 53 "wsllib_check.c"
 352  return;
 353}
 354}
 355#line 1 "Specification4_spec.o"
 356#pragma merger(0,"Specification4_spec.i","")
 357#line 10 "MinePump.h"
 358int isPumpRunning(void) ;
 359#line 11 "Specification4_spec.c"
 360__inline void __utac_acc__Specification4_spec__1(void) 
Show full sources