Showing error 1987

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

Source: 

 686  {
 687#line 209 "Environment.c"
 688  retValue_acc = waterLevel;
 689#line 211
 690  return (retValue_acc);
 691#line 218
 692  return (retValue_acc);
 693}
 694}
 695#line 58 "Environment.c"
 696int isLowWaterSensorDry(void) 
 697{ int retValue_acc ;
 698
 699  {
 700#line 240 "Environment.c"
 701  retValue_acc = waterLevel == 0;
 702#line 242
 703  return (retValue_acc);
 704#line 249
 705  return (retValue_acc);
 706}
 707}
 708#line 1 "wsllib_check.o"
 709#pragma merger(0,"wsllib_check.i","")
 710#line 3 "wsllib_check.c"
 711void __automaton_fail(void) 
 712{ 
 713
 714  {
 715  goto ERROR;
 716  ERROR: ;
 717#line 53 "wsllib_check.c"
 718  return;
 719}
 720}
 721#line 1 "scenario.o"
 722#pragma merger(0,"scenario.i","")
 723#line 7 "scenario.c"
 724#line 13
 725void timeShift(void) ;
 726#line 15
Show full sources
↑