Showing error 134

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/nested_structure_noptr-safe.cil.c
Line in file: 48
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 9 "nested_structure_noptr-safe.c"
 5struct Innermost {
 6   int c ;
 7};
 8#line 9 "nested_structure_noptr-safe.c"
 9struct Inner {
10   int b ;
11   struct Innermost y ;
12};
13#line 9 "nested_structure_noptr-safe.c"
14struct Toplev {
15   int a ;
16   struct Inner x ;
17};
18#line 71 "/usr/include/assert.h"
19extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
20                                                                      char const   *__file ,
21                                                                      unsigned int __line ,
22                                                                      char const   *__function ) ;
23#line 7 "nested_structure_noptr-safe.c"
24
25#line 19 "nested_structure_noptr-safe.c"
26int main(void) 
27{ struct Toplev good ;
28  int good_c2 ;
29  int good_b3 ;
30  int good_a4 ;
31
32  {
33#line 21
34  good_a4 = 1;
35#line 21
36  good_b3 = 2;
37#line 21
38  good_c2 = 3;
39#line 22
40  good_c2 = 4;
41#line 23
42  if (good_c2 == 4) {
43
44  } else {
45    {
46#line 23
47    //__assert_fail("good.x.y.c == 4", "nested_structure_noptr-safe.c", 23U, "main");
48    ERROR:assert(0); goto ERROR;
49    }
50  }
51#line 24
52  return (0);
53}
54}
↑