1
2
3
4#line 211 "/usr/lib/x86_64-linux-gnu/gcc/x86_64-linux-gnu/4.5.2/include/stddef.h"
5typedef unsigned long size_t;
6#line 12 "simple_built_from_end.c"
7struct node {
8 int h ;
9 struct node *n ;
10};
11#line 12 "simple_built_from_end.c"
12typedef struct node *List;
13#line 471 "/usr/include/stdlib.h"
14extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
15#line 544
16 __attribute__((__nothrow__, __noreturn__)) void exit(int s ) ;
17#line 8 "simple_built_from_end.c"
18 __attribute__((__nothrow__, __noreturn__)) void exit(int s ) ;
19#line 8 "simple_built_from_end.c"
20void exit(int s )
21{
22
23 {
24 _EXIT:
25 goto _EXIT;
26}
27}
28#line 21
29extern int ( __VERIFIER_nondet_int)() ;
30#line 17 "simple_built_from_end.c"
31int main(void)
32{ List t ;
33 List p ;
34 void *tmp ;
35 int tmp___0 ;
36 unsigned long __cil_tmp5 ;
37 List __cil_tmp6 ;
38 unsigned int __cil_tmp7 ;
39 unsigned int __cil_tmp8 ;
40 unsigned int __cil_tmp9 ;
41 unsigned int __cil_tmp10 ;
42 List __cil_tmp11 ;
43 unsigned int __cil_tmp12 ;
44 unsigned int __cil_tmp13 ;
45 int __cil_tmp14 ;
46 unsigned int __cil_tmp15 ;
47 unsigned int __cil_tmp16 ;
48
49 {
50#line 20
51 p = (List )0;
52 {
53#line 21
54 while (1) {
55 while_0_continue: ;
56 {
57#line 21
58 tmp___0 = __VERIFIER_nondet_int();
59 }
60#line 21
61 if (tmp___0) {
62
63 } else {
64 goto while_0_break;
65 }
66 {
67#line 22
68 __cil_tmp5 = (unsigned long )8U;
69#line 22
70 tmp = malloc(__cil_tmp5);
71#line 22
72 t = (struct node *)tmp;
73 }
74 {
75#line 23
76 __cil_tmp6 = (List )0;
77#line 23
78 __cil_tmp7 = (unsigned int )__cil_tmp6;
79#line 23
80 __cil_tmp8 = (unsigned int )t;
81#line 23
82 if (__cil_tmp8 == __cil_tmp7) {
83 {
84#line 23
85 exit(1);
86 }
87 } else {
88
89 }
90 }
91#line 24
92 *((int *)t) = 1;
93#line 25
94 __cil_tmp9 = (unsigned int )t;
95#line 25
96 __cil_tmp10 = __cil_tmp9 + 4;
97#line 25
98 *((struct node **)__cil_tmp10) = p;
99#line 26
100 p = t;
101 }
102 while_0_break: ;
103 }
104 {
105#line 28
106 while (1) {
107 while_1_continue: ;
108 {
109#line 28
110 __cil_tmp11 = (List )0;
111#line 28
112 __cil_tmp12 = (unsigned int )__cil_tmp11;
113#line 28
114 __cil_tmp13 = (unsigned int )p;
115#line 28
116 if (__cil_tmp13 != __cil_tmp12) {
117
118 } else {
119 goto while_1_break;
120 }
121 }
122 {
123#line 29
124 __cil_tmp14 = *((int *)p);
125#line 29
126 if (__cil_tmp14 != 1) {
127 ERROR:
128 goto ERROR;
129 } else {
130
131 }
132 }
133#line 32
134 __cil_tmp15 = (unsigned int )p;
135#line 32
136 __cil_tmp16 = __cil_tmp15 + 4;
137#line 32
138 p = *((struct node **)__cil_tmp16);
139 }
140 while_1_break: ;
141 }
142#line 35
143 return (0);
144}
145}