Showing error 149

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_address.c-safe.cil.c
Line in file: 13
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 5 "files/test_address.c"
 5struct path_info {
 6   int list ;
 7};
 8#line 2 "./assert.h"
 9void __blast_assert(void) 
10{ 
11
12  {
13  ERROR:assert(0); 
14#line 4
15  goto ERROR;
16}
17}
18#line 9 "files/test_address.c"
19void list_add(int *new ) 
20{ void *__cil_tmp2 ;
21  unsigned int __cil_tmp3 ;
22  unsigned int __cil_tmp4 ;
23
24  {
25  {
26#line 10
27  __cil_tmp2 = (void *)0;
28#line 10
29  __cil_tmp3 = (unsigned int )__cil_tmp2;
30#line 10
31  __cil_tmp4 = (unsigned int )new;
32#line 10
33  if (__cil_tmp4 != __cil_tmp3) {
34
35  } else {
36    {
37#line 10
38    __blast_assert();
39    }
40  }
41  }
42#line 11
43  return;
44}
45}
46#line 13 "files/test_address.c"
47static void rr_fail_path(struct path_info *pi ) 
48{ int *__cil_tmp2 ;
49
50  {
51  {
52#line 15
53  __cil_tmp2 = & pi->list;
54#line 15
55  list_add(__cil_tmp2);
56  }
57#line 16
58  return;
59}
60}
61#line 19 "files/test_address.c"
62int main(void) 
63{ struct path_info pi ;
64
65  {
66  {
67#line 21
68  rr_fail_path(& pi);
69  }
70#line 22
71  return (0);
72}
73}
↑