Showing error 1930

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


Source:

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