Showing error 133

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