Showing error 2003

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


Source:

 846    }
 847  }
 848#line 903 "libacc.c"
 849  __cil_tmp7 = i - 1;
 850#line 903
 851  __cil_tmp8 = (unsigned long )this;
 852#line 903
 853  __cil_tmp9 = __cil_tmp8 + 24;
 854#line 903
 855  mem_13 = (char const   ***)__cil_tmp9;
 856#line 903
 857  __cil_tmp10 = *mem_13;
 858#line 903
 859  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
 860#line 903
 861  retValue_acc = *__cil_tmp11;
 862#line 905
 863  return (retValue_acc);
 864#line 912
 865  return (retValue_acc);
 866}
 867}
 868#line 1 "wsllib_check.o"
 869#pragma merger(0,"wsllib_check.i","")
 870#line 3 "wsllib_check.c"
 871void __automaton_fail(void) 
 872{ 
 873
 874  {
 875  goto ERROR;
 876  ERROR: ;
 877#line 53 "wsllib_check.c"
 878  return;
 879}
 880}
 881#line 1 "scenario.o"
 882#pragma merger(0,"scenario.i","")
 883#line 1 "scenario.c"
 884void test(void) 
 885{ int splverifierCounter ;
 886  int tmp ;
Show full sources