Showing error 2135

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


Source:

  20   void *excep_return ;
  21};
  22#line 18 "libacc.c"
  23struct __UTAC__CFLOW_FUNC {
  24   int (*func)(int  , int  ) ;
  25   int val ;
  26   struct __UTAC__CFLOW_FUNC *next ;
  27};
  28#line 18 "libacc.c"
  29struct __UTAC__EXCEPTION {
  30   void *jumpbuf ;
  31   unsigned long long prtValue ;
  32   int pops ;
  33   struct __UTAC__CFLOW_FUNC *cflowfuncs ;
  34};
  35#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
  36typedef unsigned long size_t;
  37#line 76 "libacc.c"
  38struct __ACC__ERR {
  39   void *v ;
  40   struct __ACC__ERR *next ;
  41};
  42#line 1 "wsllib_check.o"
  43#pragma merger(0,"wsllib_check.i","")
  44#line 3 "wsllib_check.c"
  45void __automaton_fail(void) 
  46{ 
  47
  48  {
  49  goto ERROR;
  50  ERROR: ;
  51#line 53 "wsllib_check.c"
  52  return;
  53}
  54}
  55#line 1 "Test.o"
  56#pragma merger(0,"Test.i","")
  57#line 8 "Test.c"
  58int cleanupTimeShifts  =    4;
  59#line 11 "Test.c"
  60#line 20 "Test.c"
Show full sources