Showing error 2126

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_spec5_product26_safe.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  }
 688#line 903 "libacc.c"
 689  __cil_tmp7 = i - 1;
 690#line 903
 691  __cil_tmp8 = (unsigned long )this;
 692#line 903
 693  __cil_tmp9 = __cil_tmp8 + 24;
 694#line 903
 695  mem_13 = (char const   ***)__cil_tmp9;
 696#line 903
 697  __cil_tmp10 = *mem_13;
 698#line 903
 699  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
 700#line 903
 701  retValue_acc = *__cil_tmp11;
 702#line 905
 703  return (retValue_acc);
 704#line 912
 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 "MinePump.o"
 722#pragma merger(0,"MinePump.i","")
 723#line 4 "MinePump.h"
 724void timeShift(void) ;
 725#line 6
 726void activatePump(void) ;
Show full sources