Showing error 1417

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 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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: goto ERROR;
80        }
81      }
82      }
83    } else {
84
85    }
86    }
87  } else {
88
89  }
Show full sources
↑