Showing error 152

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 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

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:assert(0); goto ERROR;
64        }
65      }
66      }
67    } else {
68
69    }
70    }
71  } else {
72
73  }
Show full sources
↑