1
2
3
4#line 29 "files/rule60_list2.c"
5struct list_head {
6 struct list_head *prev ;
7 struct list_head *next ;
8};
9#line 2 "./assert.h"
10void __blast_assert(void)
11{
12
13 {
14 ERROR:assert(0);
15#line 4
16 goto ERROR;
17}
18}
19#line 11 "files/rule60_list2.c"
20extern int __VERIFIER_nondet_int(void) ;
21#line 13 "files/rule60_list2.c"
22void *guard_malloc_counter = (void *)0;
23#line 15 "files/rule60_list2.c"
24void *__getMemory(int size )
25{ int tmp ;
26
27 {
28#line 17
29 if (size > 0) {
30
31 } else {
32 {
33#line 17
34 __blast_assert();
35 }
36 }
37 {
38#line 18
39 guard_malloc_counter = guard_malloc_counter + 1;
40#line 19
41 tmp = __VERIFIER_nondet_int();
42 }
43#line 19
44 if (tmp) {
45
46 } else {
47#line 20
48 return ((void *)0);
49 }
50#line 21
51 return (guard_malloc_counter);
52}
53}
54#line 24 "files/rule60_list2.c"
55void *my_malloc(int size )
56{ void *tmp ;
57
58 {
59 {
60#line 25
61 tmp = __getMemory(size);
62 }
63#line 25
64 return (tmp);
65}
66}
67#line 33 "files/rule60_list2.c"
68struct list_head *elem = (struct list_head *)((void *)0);
69#line 35 "files/rule60_list2.c"
70static void list_add(struct list_head *new , struct list_head *head )
71{ int tmp ;
72 unsigned int __cil_tmp4 ;
73 unsigned int __cil_tmp5 ;
74
75 {
76 {
77#line 36
78 __cil_tmp4 = (unsigned int )elem;
79#line 36
80 __cil_tmp5 = (unsigned int )new;
81#line 36
82 if (__cil_tmp5 != __cil_tmp4) {
83
84 } else {
85 {
86#line 36
87 __blast_assert();
88 }
89 }
90 }
91 {
92#line 37
93 tmp = __VERIFIER_nondet_int();
94 }
95#line 37
96 if (tmp) {
97#line 38
98 elem = new;
99 } else {
100
101 }
102#line 39
103 return;
104}
105}
106#line 41 "files/rule60_list2.c"
107static void list_del(struct list_head *entry )
108{ unsigned int __cil_tmp2 ;
109 unsigned int __cil_tmp3 ;
110 void *__cil_tmp4 ;
111
112 {
113 {
114#line 42
115 __cil_tmp2 = (unsigned int )elem;
116#line 42
117 __cil_tmp3 = (unsigned int )entry;
118#line 42
119 if (__cil_tmp3 == __cil_tmp2) {
120#line 43
121 __cil_tmp4 = (void *)0;
122#line 43
123 elem = (struct list_head *)__cil_tmp4;
124 } else {
125
126 }
127 }
128#line 44
129 return;
130}
131}
132#line 46 "files/rule60_list2.c"
133static struct list_head head ;
134#line 48 "files/rule60_list2.c"
135int main(void)
136{ struct list_head *dev1 ;
137 struct list_head *dev2 ;
138 void *tmp ;
139 void *tmp___0 ;
140 int __cil_tmp5 ;
141 int __cil_tmp6 ;
142 void *__cil_tmp7 ;
143 unsigned int __cil_tmp8 ;
144 unsigned int __cil_tmp9 ;
145 void *__cil_tmp10 ;
146 unsigned int __cil_tmp11 ;
147 unsigned int __cil_tmp12 ;
148
149 {
150 {
151#line 50
152 __cil_tmp5 = (int )8U;
153#line 50
154 tmp = my_malloc(__cil_tmp5);
155#line 50
156 dev1 = (struct list_head *)tmp;
157#line 51
158 __cil_tmp6 = (int )8U;
159#line 51
160 tmp___0 = my_malloc(__cil_tmp6);
161#line 51
162 dev2 = (struct list_head *)tmp___0;
163 }
164 {
165#line 52
166 __cil_tmp7 = (void *)0;
167#line 52
168 __cil_tmp8 = (unsigned int )__cil_tmp7;
169#line 52
170 __cil_tmp9 = (unsigned int )dev1;
171#line 52
172 if (__cil_tmp9 != __cil_tmp8) {
173 {
174#line 52
175 __cil_tmp10 = (void *)0;
176#line 52
177 __cil_tmp11 = (unsigned int )__cil_tmp10;
178#line 52
179 __cil_tmp12 = (unsigned int )dev2;
180#line 52
181 if (__cil_tmp12 != __cil_tmp11) {
182 {
183#line 53
184 list_add(dev2, & head);
185#line 54
186 list_add(dev1, & head);
187#line 55
188 list_del(dev2);
189#line 56
190 list_add(dev2, & head);
191#line 59
192 list_add(dev1, & head);
193 }
194 } else {
195
196 }
197 }
198 } else {
199
200 }
201 }
202#line 62
203 return (0);
204}
205}