Showing error 151

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/test_malloc-1-safe.cil.c
Line in file: 79
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/lib/x86_64-linux-gnu/gcc/x86_64-linux-gnu/4.5.2/include/stddef.h"
 5typedef unsigned long size_t;
 6#line 71 "/usr/include/assert.h"
 7extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 8                                                                      char const   *__file ,
 9                                                                      unsigned int __line ,
10                                                                      char const   *__function ) ;
11#line 51 "/usr/include/malloc.h"
12extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
13#line 6 "test_malloc-1-safe.c"
14
15#line 7 "test_malloc-1-safe.c"
16int CURRENTLY_UNSAFE  ;
17#line 16 "test_malloc-1-safe.c"
18int main(void) 
19{ int *p1 ;
20  void *tmp ;
21  int *p2 ;
22  void *tmp___0 ;
23  unsigned long __cil_tmp5 ;
24  unsigned long __cil_tmp6 ;
25  int *__cil_tmp7 ;
26  unsigned int __cil_tmp8 ;
27  unsigned int __cil_tmp9 ;
28  int *__cil_tmp10 ;
29  unsigned int __cil_tmp11 ;
30  unsigned int __cil_tmp12 ;
31  unsigned int __cil_tmp13 ;
32  unsigned int __cil_tmp14 ;
33
34  {
35  {
36#line 18
37  __cil_tmp5 = (unsigned long )4U;
38#line 18
39  tmp = malloc(__cil_tmp5);
40#line 18
41  p1 = (int *)tmp;
42#line 19
43  __cil_tmp6 = (unsigned long )4U;
44#line 19
45  tmp___0 = malloc(__cil_tmp6);
46#line 19
47  p2 = (int *)tmp___0;
48  }
49  {
50#line 27
51  __cil_tmp7 = (int *)0;
52#line 27
53  __cil_tmp8 = (unsigned int )__cil_tmp7;
54#line 27
55  __cil_tmp9 = (unsigned int )p1;
56#line 27
57  if (__cil_tmp9 != __cil_tmp8) {
58    {
59#line 27
60    __cil_tmp10 = (int *)0;
61#line 27
62    __cil_tmp11 = (unsigned int )__cil_tmp10;
63#line 27
64    __cil_tmp12 = (unsigned int )p2;
65#line 27
66    if (__cil_tmp12 != __cil_tmp11) {
67      {
68#line 28
69      __cil_tmp13 = (unsigned int )p2;
70#line 28
71      __cil_tmp14 = (unsigned int )p1;
72#line 28
73      if (__cil_tmp14 != __cil_tmp13) {
74
75      } else {
76        {
77#line 28
78        //__assert_fail("p1!=p2", "test_malloc-1-safe.c", 28U, "main");
79        ERROR:assert(0); goto ERROR;
80        }
81      }
82      }
83    } else {
84
85    }
86    }
87  } else {
88
89  }
90  }
91#line 30
92  return (0);
93}
94}