generated_code.v 54.1 KB
Newer Older
1
2
3
4
5
6
7
8
From refinedc.lang Require Export notation.
From refinedc.lang Require Import tactics.
From refinedc.typing Require Import annotations.
Set Default Proof Using "Type".

(* Generated from [tutorial/t03_list.c]. *)
Section code.
  Definition file_0 : string := "tutorial/t03_list.c".
9
  Definition file_1 : string := "include/refinedc.h".
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
  Definition loc_2 : location_info := LocationInfo file_1 49 2 49 47.
  Definition loc_3 : location_info := LocationInfo file_1 49 9 49 46.
  Definition loc_4 : location_info := LocationInfo file_1 49 9 49 32.
  Definition loc_5 : location_info := LocationInfo file_1 49 33 49 37.
  Definition loc_6 : location_info := LocationInfo file_1 49 33 49 37.
  Definition loc_7 : location_info := LocationInfo file_1 49 39 49 45.
  Definition loc_8 : location_info := LocationInfo file_1 49 39 49 45.
  Definition loc_11 : location_info := LocationInfo file_0 170 4 170 25.
  Definition loc_12 : location_info := LocationInfo file_0 171 4 171 42.
  Definition loc_13 : location_info := LocationInfo file_0 172 4 172 42.
  Definition loc_14 : location_info := LocationInfo file_0 173 4 173 42.
  Definition loc_15 : location_info := LocationInfo file_0 175 4 175 28.
  Definition loc_16 : location_info := LocationInfo file_0 177 4 177 15.
  Definition loc_17 : location_info := LocationInfo file_0 178 4 178 15.
  Definition loc_18 : location_info := LocationInfo file_0 179 4 179 15.
  Definition loc_19 : location_info := LocationInfo file_0 181 4 181 29.
  Definition loc_20 : location_info := LocationInfo file_0 182 4 182 29.
  Definition loc_21 : location_info := LocationInfo file_0 183 4 183 29.
  Definition loc_22 : location_info := LocationInfo file_0 185 4 185 29.
  Definition loc_23 : location_info := LocationInfo file_0 187 4 187 25.
  Definition loc_24 : location_info := LocationInfo file_0 189 4 189 29.
  Definition loc_25 : location_info := LocationInfo file_0 191 4 191 23.
  Definition loc_26 : location_info := LocationInfo file_0 192 4 192 23.
  Definition loc_27 : location_info := LocationInfo file_0 193 4 193 23.
  Definition loc_28 : location_info := LocationInfo file_0 195 4 195 28.
  Definition loc_29 : location_info := LocationInfo file_0 197 4 197 32.
  Definition loc_30 : location_info := LocationInfo file_0 198 4 198 32.
  Definition loc_31 : location_info := LocationInfo file_0 199 4 199 32.
  Definition loc_32 : location_info := LocationInfo file_0 201 4 201 32.
  Definition loc_33 : location_info := LocationInfo file_0 202 4 202 32.
  Definition loc_34 : location_info := LocationInfo file_0 203 4 203 32.
  Definition loc_35 : location_info := LocationInfo file_0 203 4 203 8.
  Definition loc_36 : location_info := LocationInfo file_0 203 4 203 8.
  Definition loc_37 : location_info := LocationInfo file_0 203 9 203 23.
  Definition loc_38 : location_info := LocationInfo file_0 203 25 203 30.
  Definition loc_39 : location_info := LocationInfo file_0 203 25 203 30.
  Definition loc_40 : location_info := LocationInfo file_0 202 4 202 8.
  Definition loc_41 : location_info := LocationInfo file_0 202 4 202 8.
  Definition loc_42 : location_info := LocationInfo file_0 202 9 202 23.
  Definition loc_43 : location_info := LocationInfo file_0 202 25 202 30.
  Definition loc_44 : location_info := LocationInfo file_0 202 25 202 30.
  Definition loc_45 : location_info := LocationInfo file_0 201 4 201 8.
  Definition loc_46 : location_info := LocationInfo file_0 201 4 201 8.
  Definition loc_47 : location_info := LocationInfo file_0 201 9 201 23.
  Definition loc_48 : location_info := LocationInfo file_0 201 25 201 30.
  Definition loc_49 : location_info := LocationInfo file_0 201 25 201 30.
  Definition loc_50 : location_info := LocationInfo file_0 199 11 199 30.
  Definition loc_51 : location_info := LocationInfo file_0 199 11 199 17.
  Definition loc_52 : location_info := LocationInfo file_0 199 11 199 17.
  Definition loc_53 : location_info := LocationInfo file_0 199 12 199 17.
  Definition loc_54 : location_info := LocationInfo file_0 199 12 199 17.
  Definition loc_55 : location_info := LocationInfo file_0 199 21 199 30.
  Definition loc_56 : location_info := LocationInfo file_0 199 29 199 30.
  Definition loc_57 : location_info := LocationInfo file_0 198 11 198 30.
  Definition loc_58 : location_info := LocationInfo file_0 198 11 198 17.
  Definition loc_59 : location_info := LocationInfo file_0 198 11 198 17.
  Definition loc_60 : location_info := LocationInfo file_0 198 12 198 17.
  Definition loc_61 : location_info := LocationInfo file_0 198 12 198 17.
  Definition loc_62 : location_info := LocationInfo file_0 198 21 198 30.
  Definition loc_63 : location_info := LocationInfo file_0 198 29 198 30.
  Definition loc_64 : location_info := LocationInfo file_0 197 11 197 30.
  Definition loc_65 : location_info := LocationInfo file_0 197 11 197 17.
  Definition loc_66 : location_info := LocationInfo file_0 197 11 197 17.
  Definition loc_67 : location_info := LocationInfo file_0 197 12 197 17.
  Definition loc_68 : location_info := LocationInfo file_0 197 12 197 17.
  Definition loc_69 : location_info := LocationInfo file_0 197 21 197 30.
  Definition loc_70 : location_info := LocationInfo file_0 197 29 197 30.
  Definition loc_71 : location_info := LocationInfo file_0 195 11 195 26.
  Definition loc_72 : location_info := LocationInfo file_0 195 11 195 19.
  Definition loc_73 : location_info := LocationInfo file_0 195 11 195 19.
  Definition loc_74 : location_info := LocationInfo file_0 195 20 195 25.
  Definition loc_75 : location_info := LocationInfo file_0 195 21 195 25.
  Definition loc_76 : location_info := LocationInfo file_0 193 4 193 9.
  Definition loc_77 : location_info := LocationInfo file_0 193 12 193 22.
  Definition loc_78 : location_info := LocationInfo file_0 193 12 193 15.
  Definition loc_79 : location_info := LocationInfo file_0 193 12 193 15.
  Definition loc_80 : location_info := LocationInfo file_0 193 16 193 21.
  Definition loc_81 : location_info := LocationInfo file_0 193 17 193 21.
  Definition loc_82 : location_info := LocationInfo file_0 192 4 192 9.
  Definition loc_83 : location_info := LocationInfo file_0 192 12 192 22.
  Definition loc_84 : location_info := LocationInfo file_0 192 12 192 15.
  Definition loc_85 : location_info := LocationInfo file_0 192 12 192 15.
  Definition loc_86 : location_info := LocationInfo file_0 192 16 192 21.
  Definition loc_87 : location_info := LocationInfo file_0 192 17 192 21.
  Definition loc_88 : location_info := LocationInfo file_0 191 4 191 9.
  Definition loc_89 : location_info := LocationInfo file_0 191 12 191 22.
  Definition loc_90 : location_info := LocationInfo file_0 191 12 191 15.
  Definition loc_91 : location_info := LocationInfo file_0 191 12 191 15.
  Definition loc_92 : location_info := LocationInfo file_0 191 16 191 21.
  Definition loc_93 : location_info := LocationInfo file_0 191 17 191 21.
  Definition loc_94 : location_info := LocationInfo file_0 189 11 189 27.
  Definition loc_95 : location_info := LocationInfo file_0 189 11 189 17.
  Definition loc_96 : location_info := LocationInfo file_0 189 11 189 17.
  Definition loc_97 : location_info := LocationInfo file_0 189 18 189 23.
  Definition loc_98 : location_info := LocationInfo file_0 189 19 189 23.
  Definition loc_99 : location_info := LocationInfo file_0 189 25 189 26.
  Definition loc_100 : location_info := LocationInfo file_0 187 4 187 8.
  Definition loc_101 : location_info := LocationInfo file_0 187 11 187 24.
  Definition loc_102 : location_info := LocationInfo file_0 187 11 187 18.
  Definition loc_103 : location_info := LocationInfo file_0 187 11 187 18.
  Definition loc_104 : location_info := LocationInfo file_0 187 19 187 23.
  Definition loc_105 : location_info := LocationInfo file_0 187 19 187 23.
  Definition loc_106 : location_info := LocationInfo file_0 185 11 185 27.
  Definition loc_107 : location_info := LocationInfo file_0 185 11 185 17.
  Definition loc_108 : location_info := LocationInfo file_0 185 11 185 17.
  Definition loc_109 : location_info := LocationInfo file_0 185 18 185 23.
  Definition loc_110 : location_info := LocationInfo file_0 185 19 185 23.
  Definition loc_111 : location_info := LocationInfo file_0 185 25 185 26.
  Definition loc_112 : location_info := LocationInfo file_0 183 4 183 8.
  Definition loc_113 : location_info := LocationInfo file_0 183 11 183 28.
  Definition loc_114 : location_info := LocationInfo file_0 183 11 183 15.
  Definition loc_115 : location_info := LocationInfo file_0 183 11 183 15.
  Definition loc_116 : location_info := LocationInfo file_0 183 16 183 20.
  Definition loc_117 : location_info := LocationInfo file_0 183 16 183 20.
  Definition loc_118 : location_info := LocationInfo file_0 183 22 183 27.
  Definition loc_119 : location_info := LocationInfo file_0 183 22 183 27.
  Definition loc_120 : location_info := LocationInfo file_0 182 4 182 8.
  Definition loc_121 : location_info := LocationInfo file_0 182 11 182 28.
  Definition loc_122 : location_info := LocationInfo file_0 182 11 182 15.
  Definition loc_123 : location_info := LocationInfo file_0 182 11 182 15.
  Definition loc_124 : location_info := LocationInfo file_0 182 16 182 20.
  Definition loc_125 : location_info := LocationInfo file_0 182 16 182 20.
  Definition loc_126 : location_info := LocationInfo file_0 182 22 182 27.
  Definition loc_127 : location_info := LocationInfo file_0 182 22 182 27.
  Definition loc_128 : location_info := LocationInfo file_0 181 4 181 8.
  Definition loc_129 : location_info := LocationInfo file_0 181 11 181 28.
  Definition loc_130 : location_info := LocationInfo file_0 181 11 181 15.
  Definition loc_131 : location_info := LocationInfo file_0 181 11 181 15.
  Definition loc_132 : location_info := LocationInfo file_0 181 16 181 20.
  Definition loc_133 : location_info := LocationInfo file_0 181 16 181 20.
  Definition loc_134 : location_info := LocationInfo file_0 181 22 181 27.
  Definition loc_135 : location_info := LocationInfo file_0 181 22 181 27.
  Definition loc_136 : location_info := LocationInfo file_0 179 4 179 10.
  Definition loc_137 : location_info := LocationInfo file_0 179 5 179 10.
  Definition loc_138 : location_info := LocationInfo file_0 179 5 179 10.
  Definition loc_139 : location_info := LocationInfo file_0 179 13 179 14.
  Definition loc_140 : location_info := LocationInfo file_0 178 4 178 10.
  Definition loc_141 : location_info := LocationInfo file_0 178 5 178 10.
  Definition loc_142 : location_info := LocationInfo file_0 178 5 178 10.
  Definition loc_143 : location_info := LocationInfo file_0 178 13 178 14.
  Definition loc_144 : location_info := LocationInfo file_0 177 4 177 10.
  Definition loc_145 : location_info := LocationInfo file_0 177 5 177 10.
  Definition loc_146 : location_info := LocationInfo file_0 177 5 177 10.
  Definition loc_147 : location_info := LocationInfo file_0 177 13 177 14.
  Definition loc_148 : location_info := LocationInfo file_0 175 11 175 26.
  Definition loc_149 : location_info := LocationInfo file_0 175 11 175 19.
  Definition loc_150 : location_info := LocationInfo file_0 175 11 175 19.
  Definition loc_151 : location_info := LocationInfo file_0 175 20 175 25.
  Definition loc_152 : location_info := LocationInfo file_0 175 21 175 25.
  Definition loc_153 : location_info := LocationInfo file_0 173 20 173 41.
  Definition loc_154 : location_info := LocationInfo file_0 173 20 173 25.
  Definition loc_155 : location_info := LocationInfo file_0 173 20 173 25.
  Definition loc_156 : location_info := LocationInfo file_0 173 26 173 40.
  Definition loc_159 : location_info := LocationInfo file_0 172 20 172 41.
  Definition loc_160 : location_info := LocationInfo file_0 172 20 172 25.
  Definition loc_161 : location_info := LocationInfo file_0 172 20 172 25.
  Definition loc_162 : location_info := LocationInfo file_0 172 26 172 40.
  Definition loc_165 : location_info := LocationInfo file_0 171 20 171 41.
  Definition loc_166 : location_info := LocationInfo file_0 171 20 171 25.
  Definition loc_167 : location_info := LocationInfo file_0 171 20 171 25.
  Definition loc_168 : location_info := LocationInfo file_0 171 26 171 40.
  Definition loc_171 : location_info := LocationInfo file_0 170 18 170 24.
  Definition loc_172 : location_info := LocationInfo file_0 170 18 170 22.
  Definition loc_173 : location_info := LocationInfo file_0 170 18 170 22.
  Definition loc_178 : location_info := LocationInfo file_0 27 4 27 26.
  Definition loc_179 : location_info := LocationInfo file_0 27 11 27 25.
  Definition loc_182 : location_info := LocationInfo file_0 35 4 35 32.
  Definition loc_183 : location_info := LocationInfo file_0 35 11 35 31.
  Definition loc_184 : location_info := LocationInfo file_0 35 11 35 13.
  Definition loc_185 : location_info := LocationInfo file_0 35 11 35 13.
  Definition loc_186 : location_info := LocationInfo file_0 35 12 35 13.
  Definition loc_187 : location_info := LocationInfo file_0 35 12 35 13.
  Definition loc_188 : location_info := LocationInfo file_0 35 17 35 31.
  Definition loc_191 : location_info := LocationInfo file_0 43 4 43 51.
  Definition loc_192 : location_info := LocationInfo file_0 44 4 44 19.
  Definition loc_193 : location_info := LocationInfo file_0 45 4 45 19.
  Definition loc_194 : location_info := LocationInfo file_0 46 4 46 16.
  Definition loc_195 : location_info := LocationInfo file_0 46 11 46 15.
  Definition loc_196 : location_info := LocationInfo file_0 46 11 46 15.
  Definition loc_197 : location_info := LocationInfo file_0 45 4 45 14.
  Definition loc_198 : location_info := LocationInfo file_0 45 4 45 8.
  Definition loc_199 : location_info := LocationInfo file_0 45 4 45 8.
  Definition loc_200 : location_info := LocationInfo file_0 45 17 45 18.
  Definition loc_201 : location_info := LocationInfo file_0 45 17 45 18.
  Definition loc_202 : location_info := LocationInfo file_0 44 4 44 14.
  Definition loc_203 : location_info := LocationInfo file_0 44 4 44 8.
  Definition loc_204 : location_info := LocationInfo file_0 44 4 44 8.
  Definition loc_205 : location_info := LocationInfo file_0 44 17 44 18.
  Definition loc_206 : location_info := LocationInfo file_0 44 17 44 18.
  Definition loc_207 : location_info := LocationInfo file_0 43 24 43 50.
  Definition loc_208 : location_info := LocationInfo file_0 43 24 43 29.
  Definition loc_209 : location_info := LocationInfo file_0 43 24 43 29.
  Definition loc_210 : location_info := LocationInfo file_0 43 30 43 49.
  Definition loc_215 : location_info := LocationInfo file_0 55 2 57 3.
  Definition loc_216 : location_info := LocationInfo file_0 58 2 58 25.
  Definition loc_217 : location_info := LocationInfo file_0 59 2 59 25.
  Definition loc_218 : location_info := LocationInfo file_0 60 2 60 18.
  Definition loc_219 : location_info := LocationInfo file_0 61 2 61 34.
  Definition loc_220 : location_info := LocationInfo file_0 62 2 62 13.
  Definition loc_221 : location_info := LocationInfo file_0 62 9 62 12.
  Definition loc_222 : location_info := LocationInfo file_0 62 9 62 12.
  Definition loc_223 : location_info := LocationInfo file_0 61 2 61 6.
  Definition loc_224 : location_info := LocationInfo file_0 61 2 61 6.
  Definition loc_225 : location_info := LocationInfo file_0 61 7 61 26.
  Definition loc_226 : location_info := LocationInfo file_0 61 28 61 32.
  Definition loc_227 : location_info := LocationInfo file_0 61 28 61 32.
  Definition loc_228 : location_info := LocationInfo file_0 60 2 60 4.
  Definition loc_229 : location_info := LocationInfo file_0 60 3 60 4.
  Definition loc_230 : location_info := LocationInfo file_0 60 3 60 4.
  Definition loc_231 : location_info := LocationInfo file_0 60 7 60 17.
  Definition loc_232 : location_info := LocationInfo file_0 60 7 60 17.
  Definition loc_233 : location_info := LocationInfo file_0 60 7 60 11.
  Definition loc_234 : location_info := LocationInfo file_0 60 7 60 11.
  Definition loc_235 : location_info := LocationInfo file_0 59 14 59 24.
  Definition loc_236 : location_info := LocationInfo file_0 59 14 59 24.
  Definition loc_237 : location_info := LocationInfo file_0 59 14 59 18.
  Definition loc_238 : location_info := LocationInfo file_0 59 14 59 18.
  Definition loc_241 : location_info := LocationInfo file_0 58 22 58 24.
  Definition loc_242 : location_info := LocationInfo file_0 58 22 58 24.
  Definition loc_243 : location_info := LocationInfo file_0 58 23 58 24.
  Definition loc_244 : location_info := LocationInfo file_0 58 23 58 24.
  Definition loc_247 : location_info := LocationInfo file_0 55 28 57 3.
  Definition loc_248 : location_info := LocationInfo file_0 56 6 56 28.
  Definition loc_249 : location_info := LocationInfo file_0 56 13 56 27.
  Definition loc_251 : location_info := LocationInfo file_0 55 6 55 26.
  Definition loc_252 : location_info := LocationInfo file_0 55 6 55 8.
  Definition loc_253 : location_info := LocationInfo file_0 55 6 55 8.
  Definition loc_254 : location_info := LocationInfo file_0 55 7 55 8.
  Definition loc_255 : location_info := LocationInfo file_0 55 7 55 8.
  Definition loc_256 : location_info := LocationInfo file_0 55 12 55 26.
  Definition loc_259 : location_info := LocationInfo file_0 70 4 70 23.
  Definition loc_260 : location_info := LocationInfo file_0 74 4 79 5.
  Definition loc_261 : location_info := LocationInfo file_0 80 4 80 13.
  Definition loc_262 : location_info := LocationInfo file_0 80 11 80 12.
  Definition loc_263 : location_info := LocationInfo file_0 80 11 80 12.
  Definition loc_264 : location_info := LocationInfo file_0 74 4 79 5.
  Definition loc_265 : location_info := LocationInfo file_0 74 32 79 5.
  Definition loc_266 : location_info := LocationInfo file_0 75 8 75 20.
  Definition loc_267 : location_info := LocationInfo file_0 76 8 76 20.
  Definition loc_268 : location_info := LocationInfo file_0 77 8 77 14.
  Definition loc_269 : location_info := LocationInfo file_0 78 8 78 14.
  Definition loc_270 : location_info := LocationInfo file_0 74 4 79 5.
  Definition loc_271 : location_info := LocationInfo file_0 74 4 79 5.
  Definition loc_272 : location_info := LocationInfo file_0 78 8 78 9.
  Definition loc_273 : location_info := LocationInfo file_0 78 12 78 13.
  Definition loc_274 : location_info := LocationInfo file_0 78 12 78 13.
  Definition loc_275 : location_info := LocationInfo file_0 77 8 77 9.
  Definition loc_276 : location_info := LocationInfo file_0 77 12 77 13.
  Definition loc_277 : location_info := LocationInfo file_0 77 12 77 13.
  Definition loc_278 : location_info := LocationInfo file_0 76 8 76 15.
  Definition loc_279 : location_info := LocationInfo file_0 76 8 76 9.
  Definition loc_280 : location_info := LocationInfo file_0 76 8 76 9.
  Definition loc_281 : location_info := LocationInfo file_0 76 18 76 19.
  Definition loc_282 : location_info := LocationInfo file_0 76 18 76 19.
  Definition loc_283 : location_info := LocationInfo file_0 75 8 75 9.
  Definition loc_284 : location_info := LocationInfo file_0 75 12 75 19.
  Definition loc_285 : location_info := LocationInfo file_0 75 12 75 19.
  Definition loc_286 : location_info := LocationInfo file_0 75 12 75 13.
  Definition loc_287 : location_info := LocationInfo file_0 75 12 75 13.
  Definition loc_288 : location_info := LocationInfo file_0 74 11 74 30.
  Definition loc_289 : location_info := LocationInfo file_0 74 11 74 12.
  Definition loc_290 : location_info := LocationInfo file_0 74 11 74 12.
  Definition loc_291 : location_info := LocationInfo file_0 74 16 74 30.
  Definition loc_292 : location_info := LocationInfo file_0 70 4 70 5.
  Definition loc_293 : location_info := LocationInfo file_0 70 8 70 22.
  Definition loc_296 : location_info := LocationInfo file_0 89 2 89 17.
276
  Definition loc_297 : location_info := LocationInfo file_0 93 2 96 3.
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
  Definition loc_298 : location_info := LocationInfo file_0 97 2 97 13.
  Definition loc_299 : location_info := LocationInfo file_0 97 9 97 12.
  Definition loc_300 : location_info := LocationInfo file_0 97 9 97 12.
  Definition loc_301 : location_info := LocationInfo file_0 93 2 96 3.
  Definition loc_302 : location_info := LocationInfo file_0 93 31 96 3.
  Definition loc_303 : location_info := LocationInfo file_0 94 4 94 20.
  Definition loc_304 : location_info := LocationInfo file_0 95 4 95 13.
  Definition loc_305 : location_info := LocationInfo file_0 93 2 96 3.
  Definition loc_306 : location_info := LocationInfo file_0 93 2 96 3.
  Definition loc_307 : location_info := LocationInfo file_0 95 4 95 7.
  Definition loc_308 : location_info := LocationInfo file_0 95 4 95 12.
  Definition loc_309 : location_info := LocationInfo file_0 95 4 95 7.
  Definition loc_310 : location_info := LocationInfo file_0 95 4 95 7.
  Definition loc_311 : location_info := LocationInfo file_0 95 11 95 12.
  Definition loc_312 : location_info := LocationInfo file_0 94 4 94 5.
  Definition loc_313 : location_info := LocationInfo file_0 94 8 94 19.
  Definition loc_314 : location_info := LocationInfo file_0 94 9 94 19.
  Definition loc_315 : location_info := LocationInfo file_0 94 9 94 13.
  Definition loc_316 : location_info := LocationInfo file_0 94 9 94 13.
  Definition loc_317 : location_info := LocationInfo file_0 94 11 94 12.
  Definition loc_318 : location_info := LocationInfo file_0 94 11 94 12.
  Definition loc_319 : location_info := LocationInfo file_0 93 9 93 29.
  Definition loc_320 : location_info := LocationInfo file_0 93 9 93 11.
  Definition loc_321 : location_info := LocationInfo file_0 93 9 93 11.
  Definition loc_322 : location_info := LocationInfo file_0 93 10 93 11.
  Definition loc_323 : location_info := LocationInfo file_0 93 10 93 11.
  Definition loc_324 : location_info := LocationInfo file_0 93 15 93 29.
  Definition loc_325 : location_info := LocationInfo file_0 89 15 89 16.
  Definition loc_330 : location_info := LocationInfo file_0 106 2 108 3.
  Definition loc_331 : location_info := LocationInfo file_0 109 2 109 37.
  Definition loc_332 : location_info := LocationInfo file_0 109 9 109 36.
  Definition loc_333 : location_info := LocationInfo file_0 109 9 109 32.
  Definition loc_334 : location_info := LocationInfo file_0 109 9 109 23.
  Definition loc_335 : location_info := LocationInfo file_0 109 9 109 23.
  Definition loc_336 : location_info := LocationInfo file_0 109 24 109 31.
  Definition loc_337 : location_info := LocationInfo file_0 109 24 109 31.
  Definition loc_338 : location_info := LocationInfo file_0 109 24 109 25.
  Definition loc_339 : location_info := LocationInfo file_0 109 24 109 25.
  Definition loc_340 : location_info := LocationInfo file_0 109 35 109 36.
  Definition loc_341 : location_info := LocationInfo file_0 106 26 108 3.
  Definition loc_342 : location_info := LocationInfo file_0 107 4 107 13.
  Definition loc_343 : location_info := LocationInfo file_0 107 11 107 12.
  Definition loc_345 : location_info := LocationInfo file_0 106 5 106 24.
  Definition loc_346 : location_info := LocationInfo file_0 106 5 106 6.
  Definition loc_347 : location_info := LocationInfo file_0 106 5 106 6.
  Definition loc_348 : location_info := LocationInfo file_0 106 10 106 24.
  Definition loc_351 : location_info := LocationInfo file_0 118 2 118 17.
Michael Sammler's avatar
Michael Sammler committed
324
  Definition loc_352 : location_info := LocationInfo file_0 122 2 125 3.
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
  Definition loc_353 : location_info := LocationInfo file_0 126 2 126 13.
  Definition loc_354 : location_info := LocationInfo file_0 126 9 126 12.
  Definition loc_355 : location_info := LocationInfo file_0 126 9 126 12.
  Definition loc_356 : location_info := LocationInfo file_0 122 2 125 3.
  Definition loc_357 : location_info := LocationInfo file_0 122 30 125 3.
  Definition loc_358 : location_info := LocationInfo file_0 123 4 123 16.
  Definition loc_359 : location_info := LocationInfo file_0 124 4 124 13.
  Definition loc_360 : location_info := LocationInfo file_0 122 2 125 3.
  Definition loc_361 : location_info := LocationInfo file_0 122 2 125 3.
  Definition loc_362 : location_info := LocationInfo file_0 124 4 124 7.
  Definition loc_363 : location_info := LocationInfo file_0 124 4 124 12.
  Definition loc_364 : location_info := LocationInfo file_0 124 4 124 7.
  Definition loc_365 : location_info := LocationInfo file_0 124 4 124 7.
  Definition loc_366 : location_info := LocationInfo file_0 124 11 124 12.
  Definition loc_367 : location_info := LocationInfo file_0 123 4 123 5.
  Definition loc_368 : location_info := LocationInfo file_0 123 8 123 15.
  Definition loc_369 : location_info := LocationInfo file_0 123 8 123 15.
  Definition loc_370 : location_info := LocationInfo file_0 123 8 123 9.
  Definition loc_371 : location_info := LocationInfo file_0 123 8 123 9.
  Definition loc_372 : location_info := LocationInfo file_0 122 9 122 28.
  Definition loc_373 : location_info := LocationInfo file_0 122 9 122 10.
  Definition loc_374 : location_info := LocationInfo file_0 122 9 122 10.
  Definition loc_375 : location_info := LocationInfo file_0 122 14 122 28.
  Definition loc_376 : location_info := LocationInfo file_0 118 15 118 16.
  Definition loc_381 : location_info := LocationInfo file_0 133 2 133 19.
  Definition loc_382 : location_info := LocationInfo file_0 137 2 139 3.
  Definition loc_383 : location_info := LocationInfo file_0 140 2 140 12.
  Definition loc_384 : location_info := LocationInfo file_0 140 2 140 6.
  Definition loc_385 : location_info := LocationInfo file_0 140 3 140 6.
  Definition loc_386 : location_info := LocationInfo file_0 140 3 140 6.
  Definition loc_387 : location_info := LocationInfo file_0 140 9 140 11.
  Definition loc_388 : location_info := LocationInfo file_0 140 9 140 11.
  Definition loc_389 : location_info := LocationInfo file_0 137 2 139 3.
  Definition loc_390 : location_info := LocationInfo file_0 137 31 139 3.
  Definition loc_391 : location_info := LocationInfo file_0 138 4 138 26.
  Definition loc_392 : location_info := LocationInfo file_0 137 2 139 3.
  Definition loc_393 : location_info := LocationInfo file_0 137 2 139 3.
  Definition loc_394 : location_info := LocationInfo file_0 138 4 138 7.
  Definition loc_395 : location_info := LocationInfo file_0 138 10 138 25.
  Definition loc_396 : location_info := LocationInfo file_0 138 11 138 25.
  Definition loc_397 : location_info := LocationInfo file_0 138 12 138 18.
  Definition loc_398 : location_info := LocationInfo file_0 138 12 138 18.
  Definition loc_399 : location_info := LocationInfo file_0 138 14 138 17.
  Definition loc_400 : location_info := LocationInfo file_0 138 14 138 17.
  Definition loc_401 : location_info := LocationInfo file_0 137 8 137 30.
  Definition loc_402 : location_info := LocationInfo file_0 137 8 137 12.
  Definition loc_403 : location_info := LocationInfo file_0 137 8 137 12.
  Definition loc_404 : location_info := LocationInfo file_0 137 9 137 12.
  Definition loc_405 : location_info := LocationInfo file_0 137 9 137 12.
  Definition loc_406 : location_info := LocationInfo file_0 137 16 137 30.
  Definition loc_407 : location_info := LocationInfo file_0 133 16 133 18.
  Definition loc_408 : location_info := LocationInfo file_0 133 16 133 18.
  Definition loc_413 : location_info := LocationInfo file_0 150 4 150 21.
Michael Sammler's avatar
Michael Sammler committed
378
  Definition loc_414 : location_info := LocationInfo file_0 155 4 164 5.
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
  Definition loc_415 : location_info := LocationInfo file_0 165 4 165 13.
  Definition loc_416 : location_info := LocationInfo file_0 165 11 165 12.
  Definition loc_417 : location_info := LocationInfo file_0 155 4 164 5.
  Definition loc_418 : location_info := LocationInfo file_0 155 35 164 5.
  Definition loc_419 : location_info := LocationInfo file_0 156 8 156 27.
  Definition loc_420 : location_info := LocationInfo file_0 158 8 158 33.
  Definition loc_421 : location_info := LocationInfo file_0 159 8 161 9.
  Definition loc_422 : location_info := LocationInfo file_0 163 8 163 26.
  Definition loc_423 : location_info := LocationInfo file_0 155 4 164 5.
  Definition loc_424 : location_info := LocationInfo file_0 155 4 164 5.
  Definition loc_425 : location_info := LocationInfo file_0 163 8 163 12.
  Definition loc_426 : location_info := LocationInfo file_0 163 15 163 25.
  Definition loc_427 : location_info := LocationInfo file_0 163 16 163 25.
  Definition loc_428 : location_info := LocationInfo file_0 163 16 163 19.
  Definition loc_429 : location_info := LocationInfo file_0 163 16 163 19.
  Definition loc_430 : location_info := LocationInfo file_0 159 23 161 9.
  Definition loc_431 : location_info := LocationInfo file_0 160 12 160 21.
  Definition loc_432 : location_info := LocationInfo file_0 160 19 160 20.
  Definition loc_434 : location_info := LocationInfo file_0 159 11 159 21.
  Definition loc_435 : location_info := LocationInfo file_0 159 11 159 16.
  Definition loc_436 : location_info := LocationInfo file_0 159 11 159 16.
  Definition loc_437 : location_info := LocationInfo file_0 159 12 159 16.
  Definition loc_438 : location_info := LocationInfo file_0 159 12 159 16.
  Definition loc_439 : location_info := LocationInfo file_0 159 20 159 21.
  Definition loc_440 : location_info := LocationInfo file_0 159 20 159 21.
  Definition loc_441 : location_info := LocationInfo file_0 158 23 158 32.
  Definition loc_442 : location_info := LocationInfo file_0 158 23 158 32.
  Definition loc_443 : location_info := LocationInfo file_0 158 23 158 26.
  Definition loc_444 : location_info := LocationInfo file_0 158 23 158 26.
  Definition loc_447 : location_info := LocationInfo file_0 156 21 156 26.
  Definition loc_448 : location_info := LocationInfo file_0 156 21 156 26.
  Definition loc_449 : location_info := LocationInfo file_0 156 22 156 26.
  Definition loc_450 : location_info := LocationInfo file_0 156 22 156 26.
  Definition loc_453 : location_info := LocationInfo file_0 155 10 155 33.
  Definition loc_454 : location_info := LocationInfo file_0 155 10 155 15.
  Definition loc_455 : location_info := LocationInfo file_0 155 10 155 15.
  Definition loc_456 : location_info := LocationInfo file_0 155 11 155 15.
  Definition loc_457 : location_info := LocationInfo file_0 155 11 155 15.
  Definition loc_458 : location_info := LocationInfo file_0 155 19 155 33.
  Definition loc_459 : location_info := LocationInfo file_0 150 19 150 20.
  Definition loc_460 : location_info := LocationInfo file_0 150 19 150 20.
  Definition loc_465 : location_info := LocationInfo file_0 210 2 210 18.
  Definition loc_466 : location_info := LocationInfo file_0 220 2 225 3.
  Definition loc_467 : location_info := LocationInfo file_0 220 2 225 3.
  Definition loc_468 : location_info := LocationInfo file_0 220 31 225 3.
  Definition loc_469 : location_info := LocationInfo file_0 221 4 221 25.
  Definition loc_470 : location_info := LocationInfo file_0 222 4 222 20.
  Definition loc_471 : location_info := LocationInfo file_0 223 4 223 14.
  Definition loc_472 : location_info := LocationInfo file_0 224 4 224 19.
  Definition loc_473 : location_info := LocationInfo file_0 220 2 225 3.
  Definition loc_474 : location_info := LocationInfo file_0 220 2 225 3.
  Definition loc_475 : location_info := LocationInfo file_0 224 4 224 7.
  Definition loc_476 : location_info := LocationInfo file_0 224 10 224 18.
  Definition loc_477 : location_info := LocationInfo file_0 224 10 224 18.
  Definition loc_478 : location_info := LocationInfo file_0 223 4 223 7.
  Definition loc_479 : location_info := LocationInfo file_0 223 5 223 7.
  Definition loc_480 : location_info := LocationInfo file_0 223 5 223 7.
  Definition loc_481 : location_info := LocationInfo file_0 223 10 223 13.
  Definition loc_482 : location_info := LocationInfo file_0 223 10 223 13.
  Definition loc_483 : location_info := LocationInfo file_0 222 4 222 13.
  Definition loc_484 : location_info := LocationInfo file_0 222 4 222 7.
  Definition loc_485 : location_info := LocationInfo file_0 222 4 222 7.
  Definition loc_486 : location_info := LocationInfo file_0 222 16 222 19.
  Definition loc_487 : location_info := LocationInfo file_0 222 16 222 19.
  Definition loc_488 : location_info := LocationInfo file_0 222 17 222 19.
  Definition loc_489 : location_info := LocationInfo file_0 222 17 222 19.
  Definition loc_490 : location_info := LocationInfo file_0 221 4 221 12.
  Definition loc_491 : location_info := LocationInfo file_0 221 15 221 24.
  Definition loc_492 : location_info := LocationInfo file_0 221 15 221 24.
  Definition loc_493 : location_info := LocationInfo file_0 221 15 221 18.
  Definition loc_494 : location_info := LocationInfo file_0 221 15 221 18.
  Definition loc_495 : location_info := LocationInfo file_0 220 8 220 29.
  Definition loc_496 : location_info := LocationInfo file_0 220 8 220 11.
  Definition loc_497 : location_info := LocationInfo file_0 220 8 220 11.
  Definition loc_498 : location_info := LocationInfo file_0 220 15 220 29.
  Definition loc_499 : location_info := LocationInfo file_0 210 15 210 17.
  Definition loc_500 : location_info := LocationInfo file_0 210 15 210 17.
456
457
458
459

  (* Definition of struct [list]. *)
  Program Definition struct_list := {|
    sl_members := [
460
461
      (Some "head", void*);
      (Some "tail", void*)
462
463
464
465
    ];
  |}.
  Solve Obligations with solve_struct_obligations.

466
467
468
469
470
471
472
473
474
475
476
477
  (* Definition of function [copy_alloc_id]. *)
  Definition impl_copy_alloc_id : function := {|
    f_args := [
      ("to", it_layout uintptr_t);
      ("from", void*)
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
        locinfo: loc_2 ;
Michael Sammler's avatar
Michael Sammler committed
478
        Return (LocInfoE loc_3 (CopyAllocId (IntOp uintptr_t) (LocInfoE loc_5 (use{IntOp uintptr_t} (LocInfoE loc_6 ("to")))) (LocInfoE loc_7 (use{PtrOp} (LocInfoE loc_8 ("from"))))))
479
480
481
482
      ]> $
    )%E
  |}.

483
  (* Definition of function [test]. *)
484
  Definition impl_test (global_alloc global_free global_init global_is_empty global_member global_pop global_push global_reverse : loc): function := {|
485
486
487
    f_args := [
    ];
    f_local_vars := [
488
489
490
491
      ("list", void*);
      ("elem2", void*);
      ("elem1", void*);
      ("elem3", void*)
492
493
494
495
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
Michael Sammler's avatar
Michael Sammler committed
496
        "list" <-{ PtrOp }
497
          LocInfoE loc_171 (Call (LocInfoE loc_173 (global_init)) [@{expr}  ]) ;
Michael Sammler's avatar
Michael Sammler committed
498
        "elem1" <-{ PtrOp }
499
          LocInfoE loc_165 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_165 (Call (LocInfoE loc_167 (global_alloc)) [@{expr} LocInfoE loc_168 (i2v (it_layout size_t).(ly_size) size_t) ]))) ;
Michael Sammler's avatar
Michael Sammler committed
500
        "elem2" <-{ PtrOp }
501
          LocInfoE loc_159 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_159 (Call (LocInfoE loc_161 (global_alloc)) [@{expr} LocInfoE loc_162 (i2v (it_layout size_t).(ly_size) size_t) ]))) ;
Michael Sammler's avatar
Michael Sammler committed
502
        "elem3" <-{ PtrOp }
503
          LocInfoE loc_153 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_153 (Call (LocInfoE loc_155 (global_alloc)) [@{expr} LocInfoE loc_156 (i2v (it_layout size_t).(ly_size) size_t) ]))) ;
504
        locinfo: loc_15 ;
505
        assert: (LocInfoE loc_148 (Call (LocInfoE loc_150 (global_is_empty)) [@{expr} LocInfoE loc_151 (&(LocInfoE loc_152 ("list"))) ])) ;
506
        locinfo: loc_16 ;
Michael Sammler's avatar
Michael Sammler committed
507
        LocInfoE loc_145 (!{PtrOp} (LocInfoE loc_146 ("elem1"))) <-{ IntOp size_t }
508
          LocInfoE loc_147 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_147 (i2v 1 i32))) ;
509
        locinfo: loc_17 ;
Michael Sammler's avatar
Michael Sammler committed
510
        LocInfoE loc_141 (!{PtrOp} (LocInfoE loc_142 ("elem2"))) <-{ IntOp size_t }
511
          LocInfoE loc_143 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_143 (i2v 2 i32))) ;
512
        locinfo: loc_18 ;
Michael Sammler's avatar
Michael Sammler committed
513
        LocInfoE loc_137 (!{PtrOp} (LocInfoE loc_138 ("elem3"))) <-{ IntOp size_t }
514
          LocInfoE loc_139 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_139 (i2v 3 i32))) ;
515
        locinfo: loc_19 ;
Michael Sammler's avatar
Michael Sammler committed
516
517
518
        LocInfoE loc_128 ("list") <-{ PtrOp }
          LocInfoE loc_129 (Call (LocInfoE loc_131 (global_push)) [@{expr} LocInfoE loc_132 (use{PtrOp} (LocInfoE loc_133 ("list"))) ;
          LocInfoE loc_134 (use{PtrOp} (LocInfoE loc_135 ("elem1"))) ]) ;
519
        locinfo: loc_20 ;
Michael Sammler's avatar
Michael Sammler committed
520
521
522
        LocInfoE loc_120 ("list") <-{ PtrOp }
          LocInfoE loc_121 (Call (LocInfoE loc_123 (global_push)) [@{expr} LocInfoE loc_124 (use{PtrOp} (LocInfoE loc_125 ("list"))) ;
          LocInfoE loc_126 (use{PtrOp} (LocInfoE loc_127 ("elem2"))) ]) ;
523
        locinfo: loc_21 ;
Michael Sammler's avatar
Michael Sammler committed
524
525
526
        LocInfoE loc_112 ("list") <-{ PtrOp }
          LocInfoE loc_113 (Call (LocInfoE loc_115 (global_push)) [@{expr} LocInfoE loc_116 (use{PtrOp} (LocInfoE loc_117 ("list"))) ;
          LocInfoE loc_118 (use{PtrOp} (LocInfoE loc_119 ("elem3"))) ]) ;
527
        locinfo: loc_22 ;
528
529
        assert: (LocInfoE loc_106 (Call (LocInfoE loc_108 (global_member)) [@{expr} LocInfoE loc_109 (&(LocInfoE loc_110 ("list"))) ;
        LocInfoE loc_111 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_111 (i2v 1 i32))) ])) ;
530
        locinfo: loc_23 ;
Michael Sammler's avatar
Michael Sammler committed
531
532
        LocInfoE loc_100 ("list") <-{ PtrOp }
          LocInfoE loc_101 (Call (LocInfoE loc_103 (global_reverse)) [@{expr} LocInfoE loc_104 (use{PtrOp} (LocInfoE loc_105 ("list"))) ]) ;
533
        locinfo: loc_24 ;
534
535
        assert: (LocInfoE loc_94 (Call (LocInfoE loc_96 (global_member)) [@{expr} LocInfoE loc_97 (&(LocInfoE loc_98 ("list"))) ;
        LocInfoE loc_99 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_99 (i2v 1 i32))) ])) ;
536
        locinfo: loc_25 ;
Michael Sammler's avatar
Michael Sammler committed
537
        LocInfoE loc_88 ("elem1") <-{ PtrOp }
538
539
          LocInfoE loc_89 (Call (LocInfoE loc_91 (global_pop)) [@{expr} LocInfoE loc_92 (&(LocInfoE loc_93 ("list"))) ]) ;
        locinfo: loc_26 ;
Michael Sammler's avatar
Michael Sammler committed
540
        LocInfoE loc_82 ("elem2") <-{ PtrOp }
541
542
          LocInfoE loc_83 (Call (LocInfoE loc_85 (global_pop)) [@{expr} LocInfoE loc_86 (&(LocInfoE loc_87 ("list"))) ]) ;
        locinfo: loc_27 ;
Michael Sammler's avatar
Michael Sammler committed
543
        LocInfoE loc_76 ("elem3") <-{ PtrOp }
544
545
546
547
          LocInfoE loc_77 (Call (LocInfoE loc_79 (global_pop)) [@{expr} LocInfoE loc_80 (&(LocInfoE loc_81 ("list"))) ]) ;
        locinfo: loc_28 ;
        assert: (LocInfoE loc_71 (Call (LocInfoE loc_73 (global_is_empty)) [@{expr} LocInfoE loc_74 (&(LocInfoE loc_75 ("list"))) ])) ;
        locinfo: loc_29 ;
Michael Sammler's avatar
Michael Sammler committed
548
        assert: (LocInfoE loc_64 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_64 ((LocInfoE loc_65 (use{IntOp size_t} (LocInfoE loc_67 (!{PtrOp} (LocInfoE loc_68 ("elem1")))))) ={IntOp size_t, IntOp size_t} (LocInfoE loc_69 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_70 (i2v 1 i32)))))))) ;
549
        locinfo: loc_30 ;
Michael Sammler's avatar
Michael Sammler committed
550
        assert: (LocInfoE loc_57 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_57 ((LocInfoE loc_58 (use{IntOp size_t} (LocInfoE loc_60 (!{PtrOp} (LocInfoE loc_61 ("elem2")))))) ={IntOp size_t, IntOp size_t} (LocInfoE loc_62 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_63 (i2v 2 i32)))))))) ;
551
        locinfo: loc_31 ;
Michael Sammler's avatar
Michael Sammler committed
552
        assert: (LocInfoE loc_50 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_50 ((LocInfoE loc_51 (use{IntOp size_t} (LocInfoE loc_53 (!{PtrOp} (LocInfoE loc_54 ("elem3")))))) ={IntOp size_t, IntOp size_t} (LocInfoE loc_55 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_56 (i2v 3 i32)))))))) ;
553
554
        locinfo: loc_32 ;
        expr: (LocInfoE loc_32 (Call (LocInfoE loc_46 (global_free)) [@{expr} LocInfoE loc_47 (i2v (it_layout size_t).(ly_size) size_t) ;
Michael Sammler's avatar
Michael Sammler committed
555
        LocInfoE loc_48 (use{PtrOp} (LocInfoE loc_49 ("elem1"))) ])) ;
556
557
        locinfo: loc_33 ;
        expr: (LocInfoE loc_33 (Call (LocInfoE loc_41 (global_free)) [@{expr} LocInfoE loc_42 (i2v (it_layout size_t).(ly_size) size_t) ;
Michael Sammler's avatar
Michael Sammler committed
558
        LocInfoE loc_43 (use{PtrOp} (LocInfoE loc_44 ("elem2"))) ])) ;
559
560
        locinfo: loc_34 ;
        expr: (LocInfoE loc_34 (Call (LocInfoE loc_36 (global_free)) [@{expr} LocInfoE loc_37 (i2v (it_layout size_t).(ly_size) size_t) ;
Michael Sammler's avatar
Michael Sammler committed
561
        LocInfoE loc_38 (use{PtrOp} (LocInfoE loc_39 ("elem3"))) ])) ;
562
563
564
565
566
567
568
569
570
571
572
573
574
575
        Return (VOID)
      ]> $
    )%E
  |}.

  (* Definition of function [init]. *)
  Definition impl_init : function := {|
    f_args := [
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
576
577
        locinfo: loc_178 ;
        Return (LocInfoE loc_179 (NULL))
578
579
580
581
582
583
584
      ]> $
    )%E
  |}.

  (* Definition of function [is_empty]. *)
  Definition impl_is_empty : function := {|
    f_args := [
585
      ("l", void*)
586
587
588
589
590
591
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
592
        locinfo: loc_182 ;
Michael Sammler's avatar
Michael Sammler committed
593
        Return (LocInfoE loc_183 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_183 ((LocInfoE loc_184 (use{PtrOp} (LocInfoE loc_186 (!{PtrOp} (LocInfoE loc_187 ("l")))))) ={PtrOp, PtrOp} (LocInfoE loc_188 (NULL))))))
594
595
596
597
598
      ]> $
    )%E
  |}.

  (* Definition of function [push]. *)
599
  Definition impl_push (global_alloc : loc): function := {|
600
    f_args := [
601
602
      ("p", void*);
      ("e", void*)
603
604
    ];
    f_local_vars := [
605
      ("node", void*)
606
607
608
609
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
Michael Sammler's avatar
Michael Sammler committed
610
        "node" <-{ PtrOp }
611
612
          LocInfoE loc_207 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_207 (Call (LocInfoE loc_209 (global_alloc)) [@{expr} LocInfoE loc_210 (i2v (layout_of struct_list).(ly_size) size_t) ]))) ;
        locinfo: loc_192 ;
Michael Sammler's avatar
Michael Sammler committed
613
614
        LocInfoE loc_202 ((LocInfoE loc_203 (!{PtrOp} (LocInfoE loc_204 ("node")))) at{struct_list} "head") <-{ PtrOp }
          LocInfoE loc_205 (use{PtrOp} (LocInfoE loc_206 ("e"))) ;
615
        locinfo: loc_193 ;
Michael Sammler's avatar
Michael Sammler committed
616
617
        LocInfoE loc_197 ((LocInfoE loc_198 (!{PtrOp} (LocInfoE loc_199 ("node")))) at{struct_list} "tail") <-{ PtrOp }
          LocInfoE loc_200 (use{PtrOp} (LocInfoE loc_201 ("p"))) ;
618
        locinfo: loc_194 ;
Michael Sammler's avatar
Michael Sammler committed
619
        Return (LocInfoE loc_195 (use{PtrOp} (LocInfoE loc_196 ("node"))))
620
621
622
623
624
      ]> $
    )%E
  |}.

  (* Definition of function [pop]. *)
625
  Definition impl_pop (global_free : loc): function := {|
626
    f_args := [
627
      ("p", void*)
628
629
    ];
    f_local_vars := [
630
631
      ("node", void*);
      ("ret", void*)
632
633
634
635
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
636
        locinfo: loc_251 ;
Michael Sammler's avatar
Michael Sammler committed
637
        if: LocInfoE loc_251 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_251 ((LocInfoE loc_252 (use{PtrOp} (LocInfoE loc_254 (!{PtrOp} (LocInfoE loc_255 ("p")))))) ={PtrOp, PtrOp} (LocInfoE loc_256 (NULL)))))
638
        then
639
        locinfo: loc_248 ;
640
641
642
643
644
          Goto "#2"
        else
        Goto "#3"
      ]> $
      <[ "#1" :=
Michael Sammler's avatar
Michael Sammler committed
645
646
647
648
        "node" <-{ PtrOp }
          LocInfoE loc_241 (use{PtrOp} (LocInfoE loc_243 (!{PtrOp} (LocInfoE loc_244 ("p"))))) ;
        "ret" <-{ PtrOp }
          LocInfoE loc_235 (use{PtrOp} (LocInfoE loc_236 ((LocInfoE loc_237 (!{PtrOp} (LocInfoE loc_238 ("node")))) at{struct_list} "head"))) ;
649
        locinfo: loc_218 ;
Michael Sammler's avatar
Michael Sammler committed
650
651
        LocInfoE loc_229 (!{PtrOp} (LocInfoE loc_230 ("p"))) <-{ PtrOp }
          LocInfoE loc_231 (use{PtrOp} (LocInfoE loc_232 ((LocInfoE loc_233 (!{PtrOp} (LocInfoE loc_234 ("node")))) at{struct_list} "tail"))) ;
652
653
        locinfo: loc_219 ;
        expr: (LocInfoE loc_219 (Call (LocInfoE loc_224 (global_free)) [@{expr} LocInfoE loc_225 (i2v (layout_of struct_list).(ly_size) size_t) ;
Michael Sammler's avatar
Michael Sammler committed
654
        LocInfoE loc_226 (use{PtrOp} (LocInfoE loc_227 ("node"))) ])) ;
655
        locinfo: loc_220 ;
Michael Sammler's avatar
Michael Sammler committed
656
        Return (LocInfoE loc_221 (use{PtrOp} (LocInfoE loc_222 ("ret"))))
657
658
      ]> $
      <[ "#2" :=
659
660
        locinfo: loc_248 ;
        Return (LocInfoE loc_249 (NULL))
661
662
663
664
665
666
667
668
669
670
      ]> $
      <[ "#3" :=
        Goto "#1"
      ]> $
    )%E
  |}.

  (* Definition of function [reverse]. *)
  Definition impl_reverse : function := {|
    f_args := [
671
      ("p", void*)
672
673
    ];
    f_local_vars := [
674
675
      ("w", void*);
      ("t", void*)
676
677
678
679
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
680
        locinfo: loc_259 ;
Michael Sammler's avatar
Michael Sammler committed
681
        LocInfoE loc_292 ("w") <-{ PtrOp } LocInfoE loc_293 (NULL) ;
682
        locinfo: loc_260 ;
683
684
685
        Goto "#1"
      ]> $
      <[ "#1" :=
686
        locinfo: loc_288 ;
Michael Sammler's avatar
Michael Sammler committed
687
        if: LocInfoE loc_288 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_288 ((LocInfoE loc_289 (use{PtrOp} (LocInfoE loc_290 ("p")))) !={PtrOp, PtrOp} (LocInfoE loc_291 (NULL)))))
688
        then
689
        locinfo: loc_266 ;
690
691
          Goto "#2"
        else
692
        locinfo: loc_261 ;
693
694
695
          Goto "#3"
      ]> $
      <[ "#2" :=
696
        locinfo: loc_266 ;
Michael Sammler's avatar
Michael Sammler committed
697
698
        LocInfoE loc_283 ("t") <-{ PtrOp }
          LocInfoE loc_284 (use{PtrOp} (LocInfoE loc_285 ((LocInfoE loc_286 (!{PtrOp} (LocInfoE loc_287 ("p")))) at{struct_list} "tail"))) ;
699
        locinfo: loc_267 ;
Michael Sammler's avatar
Michael Sammler committed
700
701
        LocInfoE loc_278 ((LocInfoE loc_279 (!{PtrOp} (LocInfoE loc_280 ("p")))) at{struct_list} "tail") <-{ PtrOp }
          LocInfoE loc_281 (use{PtrOp} (LocInfoE loc_282 ("w"))) ;
702
        locinfo: loc_268 ;
Michael Sammler's avatar
Michael Sammler committed
703
704
        LocInfoE loc_275 ("w") <-{ PtrOp }
          LocInfoE loc_276 (use{PtrOp} (LocInfoE loc_277 ("p"))) ;
705
        locinfo: loc_269 ;
Michael Sammler's avatar
Michael Sammler committed
706
707
        LocInfoE loc_272 ("p") <-{ PtrOp }
          LocInfoE loc_273 (use{PtrOp} (LocInfoE loc_274 ("t"))) ;
708
709
        locinfo: loc_270 ;
        Goto "continue13"
710
711
      ]> $
      <[ "#3" :=
712
        locinfo: loc_261 ;
Michael Sammler's avatar
Michael Sammler committed
713
        Return (LocInfoE loc_262 (use{PtrOp} (LocInfoE loc_263 ("w"))))
714
      ]> $
715
716
      <[ "continue13" :=
        locinfo: loc_260 ;
717
718
719
720
721
        Goto "#1"
      ]> $
    )%E
  |}.

722
723
724
  (* Definition of function [length]. *)
  Definition impl_length : function := {|
    f_args := [
725
      ("p", void*)
726
727
728
729
730
731
732
    ];
    f_local_vars := [
      ("len", it_layout size_t)
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
Michael Sammler's avatar
Michael Sammler committed
733
        "len" <-{ IntOp size_t }
734
735
          LocInfoE loc_325 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_325 (i2v 0 i32))) ;
        locinfo: loc_297 ;
736
737
738
        Goto "#1"
      ]> $
      <[ "#1" :=
739
        locinfo: loc_319 ;
Michael Sammler's avatar
Michael Sammler committed
740
        if: LocInfoE loc_319 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_319 ((LocInfoE loc_320 (use{PtrOp} (LocInfoE loc_322 (!{PtrOp} (LocInfoE loc_323 ("p")))))) !={PtrOp, PtrOp} (LocInfoE loc_324 (NULL)))))
741
        then
742
        locinfo: loc_303 ;
743
744
          Goto "#2"
        else
745
        locinfo: loc_298 ;
746
747
748
          Goto "#3"
      ]> $
      <[ "#2" :=
749
        locinfo: loc_303 ;
Michael Sammler's avatar
Michael Sammler committed
750
751
        LocInfoE loc_312 ("p") <-{ PtrOp }
          LocInfoE loc_313 (&(LocInfoE loc_314 ((LocInfoE loc_315 (!{PtrOp} (LocInfoE loc_317 (!{PtrOp} (LocInfoE loc_318 ("p")))))) at{struct_list} "tail"))) ;
752
        locinfo: loc_304 ;
Michael Sammler's avatar
Michael Sammler committed
753
754
        LocInfoE loc_307 ("len") <-{ IntOp size_t }
          LocInfoE loc_308 ((LocInfoE loc_309 (use{IntOp size_t} (LocInfoE loc_310 ("len")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_311 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_311 (i2v 1 i32))))) ;
755
756
        locinfo: loc_305 ;
        Goto "continue17"
757
758
      ]> $
      <[ "#3" :=
759
        locinfo: loc_298 ;
Michael Sammler's avatar
Michael Sammler committed
760
        Return (LocInfoE loc_299 (use{IntOp size_t} (LocInfoE loc_300 ("len"))))
761
      ]> $
762
763
      <[ "continue17" :=
        locinfo: loc_297 ;
764
765
766
767
768
        Goto "#1"
      ]> $
    )%E
  |}.

769
770
771
  (* Definition of function [length_val_rec]. *)
  Definition impl_length_val_rec (global_length_val_rec : loc): function := {|
    f_args := [
772
      ("p", void*)
773
774
775
776
777
778
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
779
        locinfo: loc_345 ;
Michael Sammler's avatar
Michael Sammler committed
780
        if: LocInfoE loc_345 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_345 ((LocInfoE loc_346 (use{PtrOp} (LocInfoE loc_347 ("p")))) ={PtrOp, PtrOp} (LocInfoE loc_348 (NULL)))))
781
        then
782
        locinfo: loc_342 ;
783
784
          Goto "#2"
        else
785
        locinfo: loc_331 ;
786
787
788
          Goto "#3"
      ]> $
      <[ "#1" :=
789
        locinfo: loc_331 ;
Michael Sammler's avatar
Michael Sammler committed
790
        Return (LocInfoE loc_332 ((LocInfoE loc_333 (Call (LocInfoE loc_335 (global_length_val_rec)) [@{expr} LocInfoE loc_336 (use{PtrOp} (LocInfoE loc_337 ((LocInfoE loc_338 (!{PtrOp} (LocInfoE loc_339 ("p")))) at{struct_list} "tail"))) ])) +{IntOp size_t, IntOp size_t} (LocInfoE loc_340 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_340 (i2v 1 i32))))))
791
792
      ]> $
      <[ "#2" :=
793
794
        locinfo: loc_342 ;
        Return (LocInfoE loc_343 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_343 (i2v 0 i32))))
795
796
      ]> $
      <[ "#3" :=
797
        locinfo: loc_331 ;
798
799
800
801
802
        Goto "#1"
      ]> $
    )%E
  |}.

803
804
805
  (* Definition of function [length_val]. *)
  Definition impl_length_val : function := {|
    f_args := [
806
      ("p", void*)
807
808
809
810
811
812
813
    ];
    f_local_vars := [
      ("len", it_layout size_t)
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
Michael Sammler's avatar
Michael Sammler committed
814
        "len" <-{ IntOp size_t }
815
816
          LocInfoE loc_376 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_376 (i2v 0 i32))) ;
        locinfo: loc_352 ;
817
818
819
        Goto "#1"
      ]> $
      <[ "#1" :=
820
        locinfo: loc_372 ;
Michael Sammler's avatar
Michael Sammler committed
821
        if: LocInfoE loc_372 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_372 ((LocInfoE loc_373 (use{PtrOp} (LocInfoE loc_374 ("p")))) !={PtrOp, PtrOp} (LocInfoE loc_375 (NULL)))))
822
        then
823
        locinfo: loc_358 ;
824
825
          Goto "#2"
        else
826
        locinfo: loc_353 ;
827
828
829
          Goto "#3"
      ]> $
      <[ "#2" :=
830
        locinfo: loc_358 ;
Michael Sammler's avatar
Michael Sammler committed
831
832
        LocInfoE loc_367 ("p") <-{ PtrOp }
          LocInfoE loc_368 (use{PtrOp} (LocInfoE loc_369 ((LocInfoE loc_370 (!{PtrOp} (LocInfoE loc_371 ("p")))) at{struct_list} "tail"))) ;
833
        locinfo: loc_359 ;
Michael Sammler's avatar
Michael Sammler committed
834
835
        LocInfoE loc_362 ("len") <-{ IntOp size_t }
          LocInfoE loc_363 ((LocInfoE loc_364 (use{IntOp size_t} (LocInfoE loc_365 ("len")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_366 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_366 (i2v 1 i32))))) ;
836
837
        locinfo: loc_360 ;
        Goto "continue24"
838
839
      ]> $
      <[ "#3" :=
840
        locinfo: loc_353 ;
Michael Sammler's avatar
Michael Sammler committed
841
        Return (LocInfoE loc_354 (use{IntOp size_t} (LocInfoE loc_355 ("len"))))
842
      ]> $
843
844
      <[ "continue24" :=
        locinfo: loc_352 ;
845
846
847
848
849
        Goto "#1"
      ]> $
    )%E
  |}.

850
851
852
  (* Definition of function [append]. *)
  Definition impl_append : function := {|
    f_args := [
853
854
      ("l1", void*);
      ("l2", void*)
855
856
    ];
    f_local_vars := [
857
      ("end", void*)
858
859
860
861
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
Michael Sammler's avatar
Michael Sammler committed
862
863
        "end" <-{ PtrOp }
          LocInfoE loc_407 (use{PtrOp} (LocInfoE loc_408 ("l1"))) ;
864
        locinfo: loc_382 ;
865
866
867
        Goto "#1"
      ]> $
      <[ "#1" :=
868
        locinfo: loc_401 ;
Michael Sammler's avatar
Michael Sammler committed
869
        if: LocInfoE loc_401 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_401 ((LocInfoE loc_402 (use{PtrOp} (LocInfoE loc_404 (!{PtrOp} (LocInfoE loc_405 ("end")))))) !={PtrOp, PtrOp} (LocInfoE loc_406 (NULL)))))
870
        then
871
        locinfo: loc_391 ;
872
873
          Goto "#2"
        else
874
        locinfo: loc_383 ;
875
876
877
          Goto "#3"
      ]> $
      <[ "#2" :=
878
        locinfo: loc_391 ;
Michael Sammler's avatar
Michael Sammler committed
879
880
        LocInfoE loc_394 ("end") <-{ PtrOp }
          LocInfoE loc_395 (&(LocInfoE loc_396 ((LocInfoE loc_397 (!{PtrOp} (LocInfoE loc_399 (!{PtrOp} (LocInfoE loc_400 ("end")))))) at{struct_list} "tail"))) ;
881
882
        locinfo: loc_392 ;
        Goto "continue28"
883
884
      ]> $
      <[ "#3" :=
885
        locinfo: loc_383 ;
Michael Sammler's avatar
Michael Sammler committed
886
887
        LocInfoE loc_385 (!{PtrOp} (LocInfoE loc_386 ("end"))) <-{ PtrOp }
          LocInfoE loc_387 (use{PtrOp} (LocInfoE loc_388 ("l2"))) ;
888
889
        Return (VOID)
      ]> $
890
891
      <[ "continue28" :=
        locinfo: loc_382 ;
892
893
894
895
896
897
898
899
        Goto "#1"
      ]> $
    )%E
  |}.

  (* Definition of function [member]. *)
  Definition impl_member : function := {|
    f_args := [
900
      ("p", void*);
901
902
903
      ("k", it_layout size_t)
    ];
    f_local_vars := [
904
905
906
      ("prev", void*);
      ("cur", void*);
      ("head", void*)
907
908
909
910
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
Michael Sammler's avatar
Michael Sammler committed
911
912
        "prev" <-{ PtrOp }
          LocInfoE loc_459 (use{PtrOp} (LocInfoE loc_460 ("p"))) ;
913
        locinfo: loc_414 ;
914
915
916
        Goto "#1"
      ]> $
      <[ "#1" :=
917
        locinfo: loc_453 ;
Michael Sammler's avatar
Michael Sammler committed
918
        if: LocInfoE loc_453 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_453 ((LocInfoE loc_454 (use{PtrOp} (LocInfoE loc_456 (!{PtrOp} (LocInfoE loc_457 ("prev")))))) !={PtrOp, PtrOp} (LocInfoE loc_458 (NULL)))))
919
920
921
        then
        Goto "#2"
        else
922
        locinfo: loc_415