Showing error 123

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-regression/alt_test.c-unsafe.cil.c
Line in file: 15
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

  1/* Generated by CIL v. 1.3.7 */
  2/* print_CIL_Input is true */
  3
  4#line 211 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h"
  5typedef unsigned long size_t;
  6#line 471 "/usr/include/stdlib.h"
  7extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
  8#line 488
  9extern  __attribute__((__nothrow__)) void free(void *__ptr ) ;
 10#line 2 "./assert.h"
 11void __blast_assert(void) 
 12{ 
 13
 14  {
 15  ERROR:assert(0); 
 16#line 4
 17  goto ERROR;
 18}
 19}
 20#line 6 "files/alt_test.c"
 21int globalState  =    0;
 22#line 7
 23void *l_malloc(int size ) ;
 24#line 8
 25void l_free(void *ptr ) ;
 26#line 10 "files/alt_test.c"
 27int main(int argc , char **argv ) 
 28{ int *a ;
 29  void *tmp ;
 30  int __cil_tmp5 ;
 31  void *__cil_tmp6 ;
 32  void *__cil_tmp7 ;
 33
 34  {
 35  {
 36#line 12
 37  __cil_tmp5 = (int )4U;
 38#line 12
 39  tmp = l_malloc(__cil_tmp5);
 40#line 12
 41  a = (int *)tmp;
 42#line 13
 43  __cil_tmp6 = (void *)a;
 44#line 13
 45  l_free(__cil_tmp6);
 46#line 14
 47  __cil_tmp7 = (void *)a;
 48#line 14
 49  l_free(__cil_tmp7);
 50  }
 51#line 15
 52  return (0);
 53}
 54}
 55#line 18 "files/alt_test.c"
 56void *l_malloc(int size ) 
 57{ void *retVal ;
 58  void *tmp ;
 59  size_t __cil_tmp4 ;
 60  void *__cil_tmp5 ;
 61  unsigned int __cil_tmp6 ;
 62  unsigned int __cil_tmp7 ;
 63
 64  {
 65  {
 66#line 19
 67  __cil_tmp4 = (size_t )size;
 68#line 19
 69  tmp = malloc(__cil_tmp4);
 70#line 19
 71  retVal = tmp;
 72  }
 73  {
 74#line 20
 75  __cil_tmp5 = (void *)0;
 76#line 20
 77  __cil_tmp6 = (unsigned int )__cil_tmp5;
 78#line 20
 79  __cil_tmp7 = (unsigned int )retVal;
 80#line 20
 81  if (__cil_tmp7 != __cil_tmp6) {
 82#line 21
 83    globalState = 1;
 84  } else {
 85
 86  }
 87  }
 88#line 22
 89  return (retVal);
 90}
 91}
 92#line 25 "files/alt_test.c"
 93void l_free(void *ptr ) 
 94{ void *__cil_tmp2 ;
 95  unsigned int __cil_tmp3 ;
 96  unsigned int __cil_tmp4 ;
 97
 98  {
 99  {
100#line 29
101  __cil_tmp2 = (void *)0;
102#line 29
103  __cil_tmp3 = (unsigned int )__cil_tmp2;
104#line 29
105  __cil_tmp4 = (unsigned int )ptr;
106#line 29
107  if (__cil_tmp4 != __cil_tmp3) {
108#line 29
109    if (globalState == 1) {
110
111    } else {
112      {
113#line 29
114      __blast_assert();
115      }
116    }
117  } else {
118
119  }
120  }
121  {
122#line 30
123  globalState = 0;
124#line 31
125  free(ptr);
126  }
127#line 32
128  return;
129}
130}