Showing error 1419

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

Source: 

 1/* Generated by CIL v. 1.3.7 */
 2/* print_CIL_Input is true */
 3
 4#line 71 "/usr/include/assert.h"
 5extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 6                                                                      char const   *__file ,
 7                                                                      unsigned int __line ,
 8                                                                      char const   *__function ) ;
 9#line 12 "test_malloc-2-safe.c"
10
11#line 13 "test_malloc-2-safe.c"
12int CURRENTLY_UNSAFE  ;
13#line 16 "test_malloc-2-safe.c"
14int main(void) 
15{ int a ;
16  int b ;
17  int *p1 ;
18  int *p2 ;
19  int *__cil_tmp5 ;
20  unsigned int __cil_tmp6 ;
21  unsigned int __cil_tmp7 ;
22  int *__cil_tmp8 ;
23  unsigned int __cil_tmp9 ;
24  unsigned int __cil_tmp10 ;
25  unsigned int __cil_tmp11 ;
26  unsigned int __cil_tmp12 ;
27
28  {
29#line 24
30  p1 = & a;
31#line 25
32  p2 = & b;
33  {
34#line 27
35  __cil_tmp5 = (int *)0;
36#line 27
37  __cil_tmp6 = (unsigned int )__cil_tmp5;
38#line 27
39  __cil_tmp7 = (unsigned int )p1;
40#line 27
41  if (__cil_tmp7 != __cil_tmp6) {
42    {
43#line 27
44    __cil_tmp8 = (int *)0;
45#line 27
46    __cil_tmp9 = (unsigned int )__cil_tmp8;
47#line 27
48    __cil_tmp10 = (unsigned int )p2;
49#line 27
50    if (__cil_tmp10 != __cil_tmp9) {
51      {
52#line 28
53      __cil_tmp11 = (unsigned int )p2;
54#line 28
55      __cil_tmp12 = (unsigned int )p1;
56#line 28
57      if (__cil_tmp12 != __cil_tmp11) {
58
59      } else {
60        {
61#line 28
62        //__assert_fail("p1!=p2", "test_malloc-2-safe.c", 28U, "main");
63        ERROR: goto ERROR;
64        }
65      }
66      }
67    } else {
68
69    }
70    }
71  } else {
72
73  }
74  }
75#line 30
76  return (0);
77}
78}
↑