generated_code.v 53.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
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
  Definition loc_2 : location_info := LocationInfo file_0 173 4 173 25.
  Definition loc_3 : location_info := LocationInfo file_0 174 4 174 42.
  Definition loc_4 : location_info := LocationInfo file_0 175 4 175 42.
  Definition loc_5 : location_info := LocationInfo file_0 176 4 176 42.
  Definition loc_6 : location_info := LocationInfo file_0 178 4 178 28.
  Definition loc_7 : location_info := LocationInfo file_0 180 4 180 15.
  Definition loc_8 : location_info := LocationInfo file_0 181 4 181 15.
  Definition loc_9 : location_info := LocationInfo file_0 182 4 182 15.
  Definition loc_10 : location_info := LocationInfo file_0 184 4 184 29.
  Definition loc_11 : location_info := LocationInfo file_0 185 4 185 29.
  Definition loc_12 : location_info := LocationInfo file_0 186 4 186 29.
  Definition loc_13 : location_info := LocationInfo file_0 188 4 188 29.
  Definition loc_14 : location_info := LocationInfo file_0 190 4 190 25.
  Definition loc_15 : location_info := LocationInfo file_0 192 4 192 29.
  Definition loc_16 : location_info := LocationInfo file_0 194 4 194 23.
  Definition loc_17 : location_info := LocationInfo file_0 195 4 195 23.
  Definition loc_18 : location_info := LocationInfo file_0 196 4 196 23.
  Definition loc_19 : location_info := LocationInfo file_0 198 4 198 28.
  Definition loc_20 : location_info := LocationInfo file_0 200 4 200 32.
  Definition loc_21 : location_info := LocationInfo file_0 201 4 201 32.
  Definition loc_22 : location_info := LocationInfo file_0 202 4 202 32.
  Definition loc_23 : location_info := LocationInfo file_0 204 4 204 32.
  Definition loc_24 : location_info := LocationInfo file_0 205 4 205 32.
  Definition loc_25 : location_info := LocationInfo file_0 206 4 206 32.
  Definition loc_26 : location_info := LocationInfo file_0 206 4 206 8.
  Definition loc_27 : location_info := LocationInfo file_0 206 4 206 8.
  Definition loc_28 : location_info := LocationInfo file_0 206 9 206 23.
  Definition loc_29 : location_info := LocationInfo file_0 206 25 206 30.
  Definition loc_30 : location_info := LocationInfo file_0 206 25 206 30.
  Definition loc_31 : location_info := LocationInfo file_0 205 4 205 8.
  Definition loc_32 : location_info := LocationInfo file_0 205 4 205 8.
  Definition loc_33 : location_info := LocationInfo file_0 205 9 205 23.
  Definition loc_34 : location_info := LocationInfo file_0 205 25 205 30.
  Definition loc_35 : location_info := LocationInfo file_0 205 25 205 30.
  Definition loc_36 : location_info := LocationInfo file_0 204 4 204 8.
  Definition loc_37 : location_info := LocationInfo file_0 204 4 204 8.
  Definition loc_38 : location_info := LocationInfo file_0 204 9 204 23.
  Definition loc_39 : location_info := LocationInfo file_0 204 25 204 30.
  Definition loc_40 : location_info := LocationInfo file_0 204 25 204 30.
  Definition loc_41 : location_info := LocationInfo file_0 202 11 202 30.
  Definition loc_42 : location_info := LocationInfo file_0 202 11 202 17.
  Definition loc_43 : location_info := LocationInfo file_0 202 11 202 17.
  Definition loc_44 : location_info := LocationInfo file_0 202 12 202 17.
  Definition loc_45 : location_info := LocationInfo file_0 202 12 202 17.
  Definition loc_46 : location_info := LocationInfo file_0 202 21 202 30.
  Definition loc_47 : location_info := LocationInfo file_0 202 29 202 30.
  Definition loc_48 : location_info := LocationInfo file_0 201 11 201 30.
  Definition loc_49 : location_info := LocationInfo file_0 201 11 201 17.
  Definition loc_50 : location_info := LocationInfo file_0 201 11 201 17.
  Definition loc_51 : location_info := LocationInfo file_0 201 12 201 17.
  Definition loc_52 : location_info := LocationInfo file_0 201 12 201 17.
  Definition loc_53 : location_info := LocationInfo file_0 201 21 201 30.
  Definition loc_54 : location_info := LocationInfo file_0 201 29 201 30.
  Definition loc_55 : location_info := LocationInfo file_0 200 11 200 30.
  Definition loc_56 : location_info := LocationInfo file_0 200 11 200 17.
  Definition loc_57 : location_info := LocationInfo file_0 200 11 200 17.
  Definition loc_58 : location_info := LocationInfo file_0 200 12 200 17.
  Definition loc_59 : location_info := LocationInfo file_0 200 12 200 17.
  Definition loc_60 : location_info := LocationInfo file_0 200 21 200 30.
  Definition loc_61 : location_info := LocationInfo file_0 200 29 200 30.
  Definition loc_62 : location_info := LocationInfo file_0 198 11 198 26.
  Definition loc_63 : location_info := LocationInfo file_0 198 11 198 19.
  Definition loc_64 : location_info := LocationInfo file_0 198 11 198 19.
  Definition loc_65 : location_info := LocationInfo file_0 198 20 198 25.
  Definition loc_66 : location_info := LocationInfo file_0 198 21 198 25.
  Definition loc_67 : location_info := LocationInfo file_0 196 4 196 9.
  Definition loc_68 : location_info := LocationInfo file_0 196 12 196 22.
  Definition loc_69 : location_info := LocationInfo file_0 196 12 196 15.
  Definition loc_70 : location_info := LocationInfo file_0 196 12 196 15.
  Definition loc_71 : location_info := LocationInfo file_0 196 16 196 21.
  Definition loc_72 : location_info := LocationInfo file_0 196 17 196 21.
  Definition loc_73 : location_info := LocationInfo file_0 195 4 195 9.
  Definition loc_74 : location_info := LocationInfo file_0 195 12 195 22.
  Definition loc_75 : location_info := LocationInfo file_0 195 12 195 15.
  Definition loc_76 : location_info := LocationInfo file_0 195 12 195 15.
  Definition loc_77 : location_info := LocationInfo file_0 195 16 195 21.
  Definition loc_78 : location_info := LocationInfo file_0 195 17 195 21.
  Definition loc_79 : location_info := LocationInfo file_0 194 4 194 9.
  Definition loc_80 : location_info := LocationInfo file_0 194 12 194 22.
  Definition loc_81 : location_info := LocationInfo file_0 194 12 194 15.
  Definition loc_82 : location_info := LocationInfo file_0 194 12 194 15.
  Definition loc_83 : location_info := LocationInfo file_0 194 16 194 21.
  Definition loc_84 : location_info := LocationInfo file_0 194 17 194 21.
  Definition loc_85 : location_info := LocationInfo file_0 192 11 192 27.
  Definition loc_86 : location_info := LocationInfo file_0 192 11 192 17.
  Definition loc_87 : location_info := LocationInfo file_0 192 11 192 17.
  Definition loc_88 : location_info := LocationInfo file_0 192 18 192 23.
  Definition loc_89 : location_info := LocationInfo file_0 192 19 192 23.
  Definition loc_90 : location_info := LocationInfo file_0 192 25 192 26.
  Definition loc_91 : location_info := LocationInfo file_0 190 4 190 8.
  Definition loc_92 : location_info := LocationInfo file_0 190 11 190 24.
  Definition loc_93 : location_info := LocationInfo file_0 190 11 190 18.
  Definition loc_94 : location_info := LocationInfo file_0 190 11 190 18.
  Definition loc_95 : location_info := LocationInfo file_0 190 19 190 23.
  Definition loc_96 : location_info := LocationInfo file_0 190 19 190 23.
  Definition loc_97 : location_info := LocationInfo file_0 188 11 188 27.
  Definition loc_98 : location_info := LocationInfo file_0 188 11 188 17.
  Definition loc_99 : location_info := LocationInfo file_0 188 11 188 17.
  Definition loc_100 : location_info := LocationInfo file_0 188 18 188 23.
  Definition loc_101 : location_info := LocationInfo file_0 188 19 188 23.
  Definition loc_102 : location_info := LocationInfo file_0 188 25 188 26.
  Definition loc_103 : location_info := LocationInfo file_0 186 4 186 8.
  Definition loc_104 : location_info := LocationInfo file_0 186 11 186 28.
  Definition loc_105 : location_info := LocationInfo file_0 186 11 186 15.
  Definition loc_106 : location_info := LocationInfo file_0 186 11 186 15.
  Definition loc_107 : location_info := LocationInfo file_0 186 16 186 20.
  Definition loc_108 : location_info := LocationInfo file_0 186 16 186 20.
  Definition loc_109 : location_info := LocationInfo file_0 186 22 186 27.
  Definition loc_110 : location_info := LocationInfo file_0 186 22 186 27.
  Definition loc_111 : location_info := LocationInfo file_0 185 4 185 8.
  Definition loc_112 : location_info := LocationInfo file_0 185 11 185 28.
  Definition loc_113 : location_info := LocationInfo file_0 185 11 185 15.
  Definition loc_114 : location_info := LocationInfo file_0 185 11 185 15.
  Definition loc_115 : location_info := LocationInfo file_0 185 16 185 20.
  Definition loc_116 : location_info := LocationInfo file_0 185 16 185 20.
  Definition loc_117 : location_info := LocationInfo file_0 185 22 185 27.
  Definition loc_118 : location_info := LocationInfo file_0 185 22 185 27.
  Definition loc_119 : location_info := LocationInfo file_0 184 4 184 8.
  Definition loc_120 : location_info := LocationInfo file_0 184 11 184 28.
  Definition loc_121 : location_info := LocationInfo file_0 184 11 184 15.
  Definition loc_122 : location_info := LocationInfo file_0 184 11 184 15.
  Definition loc_123 : location_info := LocationInfo file_0 184 16 184 20.
  Definition loc_124 : location_info := LocationInfo file_0 184 16 184 20.
  Definition loc_125 : location_info := LocationInfo file_0 184 22 184 27.
  Definition loc_126 : location_info := LocationInfo file_0 184 22 184 27.
  Definition loc_127 : location_info := LocationInfo file_0 182 4 182 10.
  Definition loc_128 : location_info := LocationInfo file_0 182 5 182 10.
  Definition loc_129 : location_info := LocationInfo file_0 182 5 182 10.
  Definition loc_130 : location_info := LocationInfo file_0 182 13 182 14.
  Definition loc_131 : location_info := LocationInfo file_0 181 4 181 10.
  Definition loc_132 : location_info := LocationInfo file_0 181 5 181 10.
  Definition loc_133 : location_info := LocationInfo file_0 181 5 181 10.
  Definition loc_134 : location_info := LocationInfo file_0 181 13 181 14.
  Definition loc_135 : location_info := LocationInfo file_0 180 4 180 10.
  Definition loc_136 : location_info := LocationInfo file_0 180 5 180 10.
  Definition loc_137 : location_info := LocationInfo file_0 180 5 180 10.
  Definition loc_138 : location_info := LocationInfo file_0 180 13 180 14.
  Definition loc_139 : location_info := LocationInfo file_0 178 11 178 26.
  Definition loc_140 : location_info := LocationInfo file_0 178 11 178 19.
  Definition loc_141 : location_info := LocationInfo file_0 178 11 178 19.
  Definition loc_142 : location_info := LocationInfo file_0 178 20 178 25.
  Definition loc_143 : location_info := LocationInfo file_0 178 21 178 25.
  Definition loc_144 : location_info := LocationInfo file_0 176 20 176 41.
  Definition loc_145 : location_info := LocationInfo file_0 176 20 176 25.
  Definition loc_146 : location_info := LocationInfo file_0 176 20 176 25.
  Definition loc_147 : location_info := LocationInfo file_0 176 26 176 40.
  Definition loc_150 : location_info := LocationInfo file_0 175 20 175 41.
  Definition loc_151 : location_info := LocationInfo file_0 175 20 175 25.
  Definition loc_152 : location_info := LocationInfo file_0 175 20 175 25.
  Definition loc_153 : location_info := LocationInfo file_0 175 26 175 40.
  Definition loc_156 : location_info := LocationInfo file_0 174 20 174 41.
  Definition loc_157 : location_info := LocationInfo file_0 174 20 174 25.
  Definition loc_158 : location_info := LocationInfo file_0 174 20 174 25.
  Definition loc_159 : location_info := LocationInfo file_0 174 26 174 40.
  Definition loc_162 : location_info := LocationInfo file_0 173 18 173 24.
  Definition loc_163 : location_info := LocationInfo file_0 173 18 173 22.
  Definition loc_164 : location_info := LocationInfo file_0 173 18 173 22.
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
  Definition loc_169 : location_info := LocationInfo file_0 27 4 27 26.
  Definition loc_170 : location_info := LocationInfo file_0 27 11 27 25.
  Definition loc_173 : location_info := LocationInfo file_0 35 4 35 32.
  Definition loc_174 : location_info := LocationInfo file_0 35 11 35 31.
  Definition loc_175 : location_info := LocationInfo file_0 35 11 35 13.
  Definition loc_176 : location_info := LocationInfo file_0 35 11 35 13.
  Definition loc_177 : location_info := LocationInfo file_0 35 12 35 13.
  Definition loc_178 : location_info := LocationInfo file_0 35 12 35 13.
  Definition loc_179 : location_info := LocationInfo file_0 35 17 35 31.
  Definition loc_182 : location_info := LocationInfo file_0 43 4 43 51.
  Definition loc_183 : location_info := LocationInfo file_0 44 4 44 19.
  Definition loc_184 : location_info := LocationInfo file_0 45 4 45 19.
  Definition loc_185 : location_info := LocationInfo file_0 46 4 46 16.
  Definition loc_186 : location_info := LocationInfo file_0 46 11 46 15.
  Definition loc_187 : location_info := LocationInfo file_0 46 11 46 15.
  Definition loc_188 : location_info := LocationInfo file_0 45 4 45 14.
  Definition loc_189 : location_info := LocationInfo file_0 45 4 45 8.
  Definition loc_190 : location_info := LocationInfo file_0 45 4 45 8.
  Definition loc_191 : location_info := LocationInfo file_0 45 17 45 18.
  Definition loc_192 : location_info := LocationInfo file_0 45 17 45 18.
  Definition loc_193 : location_info := LocationInfo file_0 44 4 44 14.
  Definition loc_194 : location_info := LocationInfo file_0 44 4 44 8.
  Definition loc_195 : location_info := LocationInfo file_0 44 4 44 8.
  Definition loc_196 : location_info := LocationInfo file_0 44 17 44 18.
  Definition loc_197 : location_info := LocationInfo file_0 44 17 44 18.
  Definition loc_198 : location_info := LocationInfo file_0 43 24 43 50.
  Definition loc_199 : location_info := LocationInfo file_0 43 24 43 29.
  Definition loc_200 : location_info := LocationInfo file_0 43 24 43 29.
  Definition loc_201 : location_info := LocationInfo file_0 43 30 43 49.
  Definition loc_206 : location_info := LocationInfo file_0 55 2 57 3.
  Definition loc_207 : location_info := LocationInfo file_0 58 2 58 25.
  Definition loc_208 : location_info := LocationInfo file_0 59 2 59 25.
  Definition loc_209 : location_info := LocationInfo file_0 60 2 60 18.
  Definition loc_210 : location_info := LocationInfo file_0 61 2 61 34.
  Definition loc_211 : location_info := LocationInfo file_0 62 2 62 13.
  Definition loc_212 : location_info := LocationInfo file_0 62 9 62 12.
  Definition loc_213 : location_info := LocationInfo file_0 62 9 62 12.
  Definition loc_214 : location_info := LocationInfo file_0 61 2 61 6.
  Definition loc_215 : location_info := LocationInfo file_0 61 2 61 6.
  Definition loc_216 : location_info := LocationInfo file_0 61 7 61 26.
  Definition loc_217 : location_info := LocationInfo file_0 61 28 61 32.
  Definition loc_218 : location_info := LocationInfo file_0 61 28 61 32.
  Definition loc_219 : location_info := LocationInfo file_0 60 2 60 4.
  Definition loc_220 : location_info := LocationInfo file_0 60 3 60 4.
  Definition loc_221 : location_info := LocationInfo file_0 60 3 60 4.
  Definition loc_222 : location_info := LocationInfo file_0 60 7 60 17.
  Definition loc_223 : location_info := LocationInfo file_0 60 7 60 17.
  Definition loc_224 : location_info := LocationInfo file_0 60 7 60 11.
  Definition loc_225 : location_info := LocationInfo file_0 60 7 60 11.
  Definition loc_226 : location_info := LocationInfo file_0 59 14 59 24.
  Definition loc_227 : location_info := LocationInfo file_0 59 14 59 24.
  Definition loc_228 : location_info := LocationInfo file_0 59 14 59 18.
  Definition loc_229 : location_info := LocationInfo file_0 59 14 59 18.
  Definition loc_232 : location_info := LocationInfo file_0 58 22 58 24.
  Definition loc_233 : location_info := LocationInfo file_0 58 22 58 24.
  Definition loc_234 : location_info := LocationInfo file_0 58 23 58 24.
  Definition loc_235 : location_info := LocationInfo file_0 58 23 58 24.
  Definition loc_238 : location_info := LocationInfo file_0 55 28 57 3.
  Definition loc_239 : location_info := LocationInfo file_0 56 6 56 28.
  Definition loc_240 : location_info := LocationInfo file_0 56 13 56 27.
  Definition loc_242 : location_info := LocationInfo file_0 55 6 55 26.
  Definition loc_243 : location_info := LocationInfo file_0 55 6 55 8.
  Definition loc_244 : location_info := LocationInfo file_0 55 6 55 8.
  Definition loc_245 : location_info := LocationInfo file_0 55 7 55 8.
  Definition loc_246 : location_info := LocationInfo file_0 55 7 55 8.
  Definition loc_247 : location_info := LocationInfo file_0 55 12 55 26.
  Definition loc_250 : location_info := LocationInfo file_0 70 4 70 23.
  Definition loc_251 : location_info := LocationInfo file_0 74 4 79 5.
  Definition loc_252 : location_info := LocationInfo file_0 80 4 80 13.
  Definition loc_253 : location_info := LocationInfo file_0 80 11 80 12.
  Definition loc_254 : location_info := LocationInfo file_0 80 11 80 12.
  Definition loc_255 : location_info := LocationInfo file_0 74 4 79 5.
  Definition loc_256 : location_info := LocationInfo file_0 74 32 79 5.
  Definition loc_257 : location_info := LocationInfo file_0 75 8 75 20.
  Definition loc_258 : location_info := LocationInfo file_0 76 8 76 20.
  Definition loc_259 : location_info := LocationInfo file_0 77 8 77 14.
  Definition loc_260 : location_info := LocationInfo file_0 78 8 78 14.
  Definition loc_261 : location_info := LocationInfo file_0 74 4 79 5.
  Definition loc_262 : location_info := LocationInfo file_0 74 4 79 5.
  Definition loc_263 : location_info := LocationInfo file_0 78 8 78 9.
  Definition loc_264 : location_info := LocationInfo file_0 78 12 78 13.
  Definition loc_265 : location_info := LocationInfo file_0 78 12 78 13.
  Definition loc_266 : location_info := LocationInfo file_0 77 8 77 9.
  Definition loc_267 : location_info := LocationInfo file_0 77 12 77 13.
  Definition loc_268 : location_info := LocationInfo file_0 77 12 77 13.
  Definition loc_269 : location_info := LocationInfo file_0 76 8 76 15.
  Definition loc_270 : location_info := LocationInfo file_0 76 8 76 9.
  Definition loc_271 : location_info := LocationInfo file_0 76 8 76 9.
  Definition loc_272 : location_info := LocationInfo file_0 76 18 76 19.
  Definition loc_273 : location_info := LocationInfo file_0 76 18 76 19.
  Definition loc_274 : location_info := LocationInfo file_0 75 8 75 9.
  Definition loc_275 : location_info := LocationInfo file_0 75 12 75 19.
  Definition loc_276 : location_info := LocationInfo file_0 75 12 75 19.
  Definition loc_277 : location_info := LocationInfo file_0 75 12 75 13.
  Definition loc_278 : location_info := LocationInfo file_0 75 12 75 13.
  Definition loc_279 : location_info := LocationInfo file_0 74 11 74 30.
  Definition loc_280 : location_info := LocationInfo file_0 74 11 74 12.
  Definition loc_281 : location_info := LocationInfo file_0 74 11 74 12.
  Definition loc_282 : location_info := LocationInfo file_0 74 16 74 30.
  Definition loc_283 : location_info := LocationInfo file_0 70 4 70 5.
  Definition loc_284 : location_info := LocationInfo file_0 70 8 70 22.
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
  Definition loc_287 : location_info := LocationInfo file_0 89 2 89 17.
  Definition loc_288 : location_info := LocationInfo file_0 93 2 96 3.
  Definition loc_289 : location_info := LocationInfo file_0 97 2 97 13.
  Definition loc_290 : location_info := LocationInfo file_0 97 9 97 12.
  Definition loc_291 : location_info := LocationInfo file_0 97 9 97 12.
  Definition loc_292 : location_info := LocationInfo file_0 93 2 96 3.
  Definition loc_293 : location_info := LocationInfo file_0 93 31 96 3.
  Definition loc_294 : location_info := LocationInfo file_0 94 4 94 20.
  Definition loc_295 : location_info := LocationInfo file_0 95 4 95 13.
  Definition loc_296 : location_info := LocationInfo file_0 93 2 96 3.
  Definition loc_297 : location_info := LocationInfo file_0 93 2 96 3.
  Definition loc_298 : location_info := LocationInfo file_0 95 4 95 7.
  Definition loc_299 : location_info := LocationInfo file_0 95 4 95 12.
  Definition loc_300 : location_info := LocationInfo file_0 95 4 95 7.
  Definition loc_301 : location_info := LocationInfo file_0 95 4 95 7.
  Definition loc_302 : location_info := LocationInfo file_0 95 11 95 12.
  Definition loc_303 : location_info := LocationInfo file_0 94 4 94 5.
  Definition loc_304 : location_info := LocationInfo file_0 94 8 94 19.
  Definition loc_305 : location_info := LocationInfo file_0 94 9 94 19.
  Definition loc_306 : location_info := LocationInfo file_0 94 9 94 13.
  Definition loc_307 : location_info := LocationInfo file_0 94 9 94 13.
  Definition loc_308 : location_info := LocationInfo file_0 94 11 94 12.
  Definition loc_309 : location_info := LocationInfo file_0 94 11 94 12.
  Definition loc_310 : location_info := LocationInfo file_0 93 9 93 29.
  Definition loc_311 : location_info := LocationInfo file_0 93 9 93 11.
  Definition loc_312 : location_info := LocationInfo file_0 93 9 93 11.
  Definition loc_313 : location_info := LocationInfo file_0 93 10 93 11.
  Definition loc_314 : location_info := LocationInfo file_0 93 10 93 11.
  Definition loc_315 : location_info := LocationInfo file_0 93 15 93 29.
  Definition loc_316 : location_info := LocationInfo file_0 89 15 89 16.
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
  Definition loc_321 : location_info := LocationInfo file_0 107 2 109 3.
  Definition loc_322 : location_info := LocationInfo file_0 110 2 110 37.
  Definition loc_323 : location_info := LocationInfo file_0 110 9 110 36.
  Definition loc_324 : location_info := LocationInfo file_0 110 9 110 32.
  Definition loc_325 : location_info := LocationInfo file_0 110 9 110 23.
  Definition loc_326 : location_info := LocationInfo file_0 110 9 110 23.
  Definition loc_327 : location_info := LocationInfo file_0 110 24 110 31.
  Definition loc_328 : location_info := LocationInfo file_0 110 24 110 31.
  Definition loc_329 : location_info := LocationInfo file_0 110 24 110 25.
  Definition loc_330 : location_info := LocationInfo file_0 110 24 110 25.
  Definition loc_331 : location_info := LocationInfo file_0 110 35 110 36.
  Definition loc_332 : location_info := LocationInfo file_0 107 26 109 3.
  Definition loc_333 : location_info := LocationInfo file_0 108 4 108 13.
  Definition loc_334 : location_info := LocationInfo file_0 108 11 108 12.
  Definition loc_336 : location_info := LocationInfo file_0 107 5 107 24.
  Definition loc_337 : location_info := LocationInfo file_0 107 5 107 6.
  Definition loc_338 : location_info := LocationInfo file_0 107 5 107 6.
  Definition loc_339 : location_info := LocationInfo file_0 107 10 107 24.
315
316
317
318
319
320
321
322
323
324
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
378
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
  Definition loc_342 : location_info := LocationInfo file_0 120 2 120 17.
  Definition loc_343 : location_info := LocationInfo file_0 125 2 128 3.
  Definition loc_344 : location_info := LocationInfo file_0 129 2 129 13.
  Definition loc_345 : location_info := LocationInfo file_0 129 9 129 12.
  Definition loc_346 : location_info := LocationInfo file_0 129 9 129 12.
  Definition loc_347 : location_info := LocationInfo file_0 125 2 128 3.
  Definition loc_348 : location_info := LocationInfo file_0 125 30 128 3.
  Definition loc_349 : location_info := LocationInfo file_0 126 4 126 16.
  Definition loc_350 : location_info := LocationInfo file_0 127 4 127 13.
  Definition loc_351 : location_info := LocationInfo file_0 125 2 128 3.
  Definition loc_352 : location_info := LocationInfo file_0 125 2 128 3.
  Definition loc_353 : location_info := LocationInfo file_0 127 4 127 7.
  Definition loc_354 : location_info := LocationInfo file_0 127 4 127 12.
  Definition loc_355 : location_info := LocationInfo file_0 127 4 127 7.
  Definition loc_356 : location_info := LocationInfo file_0 127 4 127 7.
  Definition loc_357 : location_info := LocationInfo file_0 127 11 127 12.
  Definition loc_358 : location_info := LocationInfo file_0 126 4 126 5.
  Definition loc_359 : location_info := LocationInfo file_0 126 8 126 15.
  Definition loc_360 : location_info := LocationInfo file_0 126 8 126 15.
  Definition loc_361 : location_info := LocationInfo file_0 126 8 126 9.
  Definition loc_362 : location_info := LocationInfo file_0 126 8 126 9.
  Definition loc_363 : location_info := LocationInfo file_0 125 9 125 28.
  Definition loc_364 : location_info := LocationInfo file_0 125 9 125 10.
  Definition loc_365 : location_info := LocationInfo file_0 125 9 125 10.
  Definition loc_366 : location_info := LocationInfo file_0 125 14 125 28.
  Definition loc_367 : location_info := LocationInfo file_0 120 15 120 16.
  Definition loc_372 : location_info := LocationInfo file_0 136 2 136 19.
  Definition loc_373 : location_info := LocationInfo file_0 140 2 142 3.
  Definition loc_374 : location_info := LocationInfo file_0 143 2 143 12.
  Definition loc_375 : location_info := LocationInfo file_0 143 2 143 6.
  Definition loc_376 : location_info := LocationInfo file_0 143 3 143 6.
  Definition loc_377 : location_info := LocationInfo file_0 143 3 143 6.
  Definition loc_378 : location_info := LocationInfo file_0 143 9 143 11.
  Definition loc_379 : location_info := LocationInfo file_0 143 9 143 11.
  Definition loc_380 : location_info := LocationInfo file_0 140 2 142 3.
  Definition loc_381 : location_info := LocationInfo file_0 140 31 142 3.
  Definition loc_382 : location_info := LocationInfo file_0 141 4 141 26.
  Definition loc_383 : location_info := LocationInfo file_0 140 2 142 3.
  Definition loc_384 : location_info := LocationInfo file_0 140 2 142 3.
  Definition loc_385 : location_info := LocationInfo file_0 141 4 141 7.
  Definition loc_386 : location_info := LocationInfo file_0 141 10 141 25.
  Definition loc_387 : location_info := LocationInfo file_0 141 11 141 25.
  Definition loc_388 : location_info := LocationInfo file_0 141 12 141 18.
  Definition loc_389 : location_info := LocationInfo file_0 141 12 141 18.
  Definition loc_390 : location_info := LocationInfo file_0 141 14 141 17.
  Definition loc_391 : location_info := LocationInfo file_0 141 14 141 17.
  Definition loc_392 : location_info := LocationInfo file_0 140 8 140 30.
  Definition loc_393 : location_info := LocationInfo file_0 140 8 140 12.
  Definition loc_394 : location_info := LocationInfo file_0 140 8 140 12.
  Definition loc_395 : location_info := LocationInfo file_0 140 9 140 12.
  Definition loc_396 : location_info := LocationInfo file_0 140 9 140 12.
  Definition loc_397 : location_info := LocationInfo file_0 140 16 140 30.
  Definition loc_398 : location_info := LocationInfo file_0 136 16 136 18.
  Definition loc_399 : location_info := LocationInfo file_0 136 16 136 18.
  Definition loc_404 : location_info := LocationInfo file_0 153 4 153 21.
  Definition loc_405 : location_info := LocationInfo file_0 158 4 167 5.
  Definition loc_406 : location_info := LocationInfo file_0 168 4 168 13.
  Definition loc_407 : location_info := LocationInfo file_0 168 11 168 12.
  Definition loc_408 : location_info := LocationInfo file_0 158 4 167 5.
  Definition loc_409 : location_info := LocationInfo file_0 158 35 167 5.
  Definition loc_410 : location_info := LocationInfo file_0 159 8 159 27.
  Definition loc_411 : location_info := LocationInfo file_0 161 8 161 33.
  Definition loc_412 : location_info := LocationInfo file_0 162 8 164 9.
  Definition loc_413 : location_info := LocationInfo file_0 166 8 166 26.
  Definition loc_414 : location_info := LocationInfo file_0 158 4 167 5.
  Definition loc_415 : location_info := LocationInfo file_0 158 4 167 5.
  Definition loc_416 : location_info := LocationInfo file_0 166 8 166 12.
  Definition loc_417 : location_info := LocationInfo file_0 166 15 166 25.
  Definition loc_418 : location_info := LocationInfo file_0 166 16 166 25.
  Definition loc_419 : location_info := LocationInfo file_0 166 16 166 19.
  Definition loc_420 : location_info := LocationInfo file_0 166 16 166 19.
  Definition loc_421 : location_info := LocationInfo file_0 162 23 164 9.
  Definition loc_422 : location_info := LocationInfo file_0 163 12 163 21.
  Definition loc_423 : location_info := LocationInfo file_0 163 19 163 20.
  Definition loc_425 : location_info := LocationInfo file_0 162 11 162 21.
  Definition loc_426 : location_info := LocationInfo file_0 162 11 162 16.
  Definition loc_427 : location_info := LocationInfo file_0 162 11 162 16.
  Definition loc_428 : location_info := LocationInfo file_0 162 12 162 16.
  Definition loc_429 : location_info := LocationInfo file_0 162 12 162 16.
  Definition loc_430 : location_info := LocationInfo file_0 162 20 162 21.
  Definition loc_431 : location_info := LocationInfo file_0 162 20 162 21.
  Definition loc_432 : location_info := LocationInfo file_0 161 23 161 32.
  Definition loc_433 : location_info := LocationInfo file_0 161 23 161 32.
  Definition loc_434 : location_info := LocationInfo file_0 161 23 161 26.
  Definition loc_435 : location_info := LocationInfo file_0 161 23 161 26.
  Definition loc_438 : location_info := LocationInfo file_0 159 21 159 26.
  Definition loc_439 : location_info := LocationInfo file_0 159 21 159 26.
  Definition loc_440 : location_info := LocationInfo file_0 159 22 159 26.
  Definition loc_441 : location_info := LocationInfo file_0 159 22 159 26.
  Definition loc_444 : location_info := LocationInfo file_0 158 10 158 33.
  Definition loc_445 : location_info := LocationInfo file_0 158 10 158 15.
  Definition loc_446 : location_info := LocationInfo file_0 158 10 158 15.
  Definition loc_447 : location_info := LocationInfo file_0 158 11 158 15.
  Definition loc_448 : location_info := LocationInfo file_0 158 11 158 15.
  Definition loc_449 : location_info := LocationInfo file_0 158 19 158 33.
  Definition loc_450 : location_info := LocationInfo file_0 153 19 153 20.
  Definition loc_451 : location_info := LocationInfo file_0 153 19 153 20.
  Definition loc_456 : location_info := LocationInfo file_0 213 2 213 18.
  Definition loc_457 : location_info := LocationInfo file_0 223 2 228 3.
  Definition loc_458 : location_info := LocationInfo file_0 223 2 228 3.
  Definition loc_459 : location_info := LocationInfo file_0 223 31 228 3.
  Definition loc_460 : location_info := LocationInfo file_0 224 4 224 25.
  Definition loc_461 : location_info := LocationInfo file_0 225 4 225 20.
  Definition loc_462 : location_info := LocationInfo file_0 226 4 226 14.
  Definition loc_463 : location_info := LocationInfo file_0 227 4 227 19.
  Definition loc_464 : location_info := LocationInfo file_0 223 2 228 3.
  Definition loc_465 : location_info := LocationInfo file_0 223 2 228 3.
  Definition loc_466 : location_info := LocationInfo file_0 227 4 227 7.
  Definition loc_467 : location_info := LocationInfo file_0 227 10 227 18.
  Definition loc_468 : location_info := LocationInfo file_0 227 10 227 18.
  Definition loc_469 : location_info := LocationInfo file_0 226 4 226 7.
  Definition loc_470 : location_info := LocationInfo file_0 226 5 226 7.
  Definition loc_471 : location_info := LocationInfo file_0 226 5 226 7.
  Definition loc_472 : location_info := LocationInfo file_0 226 10 226 13.
  Definition loc_473 : location_info := LocationInfo file_0 226 10 226 13.
  Definition loc_474 : location_info := LocationInfo file_0 225 4 225 13.
  Definition loc_475 : location_info := LocationInfo file_0 225 4 225 7.
  Definition loc_476 : location_info := LocationInfo file_0 225 4 225 7.
  Definition loc_477 : location_info := LocationInfo file_0 225 16 225 19.
  Definition loc_478 : location_info := LocationInfo file_0 225 16 225 19.
  Definition loc_479 : location_info := LocationInfo file_0 225 17 225 19.
  Definition loc_480 : location_info := LocationInfo file_0 225 17 225 19.
  Definition loc_481 : location_info := LocationInfo file_0 224 4 224 12.
  Definition loc_482 : location_info := LocationInfo file_0 224 15 224 24.
  Definition loc_483 : location_info := LocationInfo file_0 224 15 224 24.
  Definition loc_484 : location_info := LocationInfo file_0 224 15 224 18.
  Definition loc_485 : location_info := LocationInfo file_0 224 15 224 18.
  Definition loc_486 : location_info := LocationInfo file_0 223 8 223 29.
  Definition loc_487 : location_info := LocationInfo file_0 223 8 223 11.
  Definition loc_488 : location_info := LocationInfo file_0 223 8 223 11.
  Definition loc_489 : location_info := LocationInfo file_0 223 15 223 29.
  Definition loc_490 : location_info := LocationInfo file_0 213 15 213 17.
  Definition loc_491 : location_info := LocationInfo file_0 213 15 213 17.
448
449
450
451

  (* Definition of struct [list]. *)
  Program Definition struct_list := {|
    sl_members := [
452
453
      (Some "head", void*);
      (Some "tail", void*)
454
455
456
457
458
    ];
  |}.
  Solve Obligations with solve_struct_obligations.

  (* Definition of function [test]. *)
459
  Definition impl_test (global_alloc global_free global_init global_is_empty global_member global_pop global_push global_reverse : loc): function := {|
460
461
462
    f_args := [
    ];
    f_local_vars := [
463
464
465
466
      ("list", void*);
      ("elem2", void*);
      ("elem1", void*);
      ("elem3", void*)
467
468
469
470
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
471
472
        "list" <-{ void* }
          LocInfoE loc_162 (Call (LocInfoE loc_164 (global_init)) [@{expr}  ]) ;
473
        "elem1" <-{ void* }
474
          LocInfoE loc_156 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_156 (Call (LocInfoE loc_158 (global_alloc)) [@{expr} LocInfoE loc_159 (i2v (it_layout size_t).(ly_size) size_t) ]))) ;
475
        "elem2" <-{ void* }
476
          LocInfoE loc_150 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_150 (Call (LocInfoE loc_152 (global_alloc)) [@{expr} LocInfoE loc_153 (i2v (it_layout size_t).(ly_size) size_t) ]))) ;
477
        "elem3" <-{ void* }
478
          LocInfoE loc_144 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_144 (Call (LocInfoE loc_146 (global_alloc)) [@{expr} LocInfoE loc_147 (i2v (it_layout size_t).(ly_size) size_t) ]))) ;
479
        locinfo: loc_6 ;
480
        assert: (LocInfoE loc_139 (Call (LocInfoE loc_141 (global_is_empty)) [@{expr} LocInfoE loc_142 (&(LocInfoE loc_143 ("list"))) ])) ;
481
        locinfo: loc_7 ;
482
        LocInfoE loc_136 (!{void*} (LocInfoE loc_137 ("elem1"))) <-{ it_layout size_t }
483
484
          LocInfoE loc_138 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_138 (i2v 1 i32))) ;
        locinfo: loc_8 ;
485
        LocInfoE loc_132 (!{void*} (LocInfoE loc_133 ("elem2"))) <-{ it_layout size_t }
486
487
          LocInfoE loc_134 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_134 (i2v 2 i32))) ;
        locinfo: loc_9 ;
488
        LocInfoE loc_128 (!{void*} (LocInfoE loc_129 ("elem3"))) <-{ it_layout size_t }
489
490
          LocInfoE loc_130 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_130 (i2v 3 i32))) ;
        locinfo: loc_10 ;
491
492
493
        LocInfoE loc_119 ("list") <-{ void* }
          LocInfoE loc_120 (Call (LocInfoE loc_122 (global_push)) [@{expr} LocInfoE loc_123 (use{void*} (LocInfoE loc_124 ("list"))) ;
          LocInfoE loc_125 (use{void*} (LocInfoE loc_126 ("elem1"))) ]) ;
494
        locinfo: loc_11 ;
495
496
497
        LocInfoE loc_111 ("list") <-{ void* }
          LocInfoE loc_112 (Call (LocInfoE loc_114 (global_push)) [@{expr} LocInfoE loc_115 (use{void*} (LocInfoE loc_116 ("list"))) ;
          LocInfoE loc_117 (use{void*} (LocInfoE loc_118 ("elem2"))) ]) ;
498
        locinfo: loc_12 ;
499
500
501
        LocInfoE loc_103 ("list") <-{ void* }
          LocInfoE loc_104 (Call (LocInfoE loc_106 (global_push)) [@{expr} LocInfoE loc_107 (use{void*} (LocInfoE loc_108 ("list"))) ;
          LocInfoE loc_109 (use{void*} (LocInfoE loc_110 ("elem3"))) ]) ;
502
        locinfo: loc_13 ;
503
504
        assert: (LocInfoE loc_97 (Call (LocInfoE loc_99 (global_member)) [@{expr} LocInfoE loc_100 (&(LocInfoE loc_101 ("list"))) ;
        LocInfoE loc_102 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_102 (i2v 1 i32))) ])) ;
505
        locinfo: loc_14 ;
506
507
        LocInfoE loc_91 ("list") <-{ void* }
          LocInfoE loc_92 (Call (LocInfoE loc_94 (global_reverse)) [@{expr} LocInfoE loc_95 (use{void*} (LocInfoE loc_96 ("list"))) ]) ;
508
        locinfo: loc_15 ;
509
510
        assert: (LocInfoE loc_85 (Call (LocInfoE loc_87 (global_member)) [@{expr} LocInfoE loc_88 (&(LocInfoE loc_89 ("list"))) ;
        LocInfoE loc_90 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_90 (i2v 1 i32))) ])) ;
511
        locinfo: loc_16 ;
512
513
        LocInfoE loc_79 ("elem1") <-{ void* }
          LocInfoE loc_80 (Call (LocInfoE loc_82 (global_pop)) [@{expr} LocInfoE loc_83 (&(LocInfoE loc_84 ("list"))) ]) ;
514
        locinfo: loc_17 ;
515
516
        LocInfoE loc_73 ("elem2") <-{ void* }
          LocInfoE loc_74 (Call (LocInfoE loc_76 (global_pop)) [@{expr} LocInfoE loc_77 (&(LocInfoE loc_78 ("list"))) ]) ;
517
        locinfo: loc_18 ;
518
519
        LocInfoE loc_67 ("elem3") <-{ void* }
          LocInfoE loc_68 (Call (LocInfoE loc_70 (global_pop)) [@{expr} LocInfoE loc_71 (&(LocInfoE loc_72 ("list"))) ]) ;
520
        locinfo: loc_19 ;
521
        assert: (LocInfoE loc_62 (Call (LocInfoE loc_64 (global_is_empty)) [@{expr} LocInfoE loc_65 (&(LocInfoE loc_66 ("list"))) ])) ;
522
        locinfo: loc_20 ;
523
        assert: (LocInfoE loc_55 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_55 ((LocInfoE loc_56 (use{it_layout size_t} (LocInfoE loc_58 (!{void*} (LocInfoE loc_59 ("elem1")))))) ={IntOp size_t, IntOp size_t} (LocInfoE loc_60 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_61 (i2v 1 i32)))))))) ;
524
        locinfo: loc_21 ;
525
        assert: (LocInfoE loc_48 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_48 ((LocInfoE loc_49 (use{it_layout size_t} (LocInfoE loc_51 (!{void*} (LocInfoE loc_52 ("elem2")))))) ={IntOp size_t, IntOp size_t} (LocInfoE loc_53 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_54 (i2v 2 i32)))))))) ;
526
        locinfo: loc_22 ;
527
        assert: (LocInfoE loc_41 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_41 ((LocInfoE loc_42 (use{it_layout size_t} (LocInfoE loc_44 (!{void*} (LocInfoE loc_45 ("elem3")))))) ={IntOp size_t, IntOp size_t} (LocInfoE loc_46 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_47 (i2v 3 i32)))))))) ;
528
        locinfo: loc_23 ;
529
530
        expr: (LocInfoE loc_23 (Call (LocInfoE loc_37 (global_free)) [@{expr} LocInfoE loc_38 (i2v (it_layout size_t).(ly_size) size_t) ;
        LocInfoE loc_39 (use{void*} (LocInfoE loc_40 ("elem1"))) ])) ;
531
        locinfo: loc_24 ;
532
533
        expr: (LocInfoE loc_24 (Call (LocInfoE loc_32 (global_free)) [@{expr} LocInfoE loc_33 (i2v (it_layout size_t).(ly_size) size_t) ;
        LocInfoE loc_34 (use{void*} (LocInfoE loc_35 ("elem2"))) ])) ;
534
        locinfo: loc_25 ;
535
536
        expr: (LocInfoE loc_25 (Call (LocInfoE loc_27 (global_free)) [@{expr} LocInfoE loc_28 (i2v (it_layout size_t).(ly_size) size_t) ;
        LocInfoE loc_29 (use{void*} (LocInfoE loc_30 ("elem3"))) ])) ;
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
        Return (VOID)
      ]> $
    )%E
  |}.

  (* Definition of function [init]. *)
  Definition impl_init : function := {|
    f_args := [
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
        locinfo: loc_169 ;
        Return (LocInfoE loc_170 (NULL))
      ]> $
    )%E
  |}.

  (* Definition of function [is_empty]. *)
  Definition impl_is_empty : function := {|
    f_args := [
560
      ("l", void*)
561
562
563
564
565
566
567
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
        locinfo: loc_173 ;
568
        Return (LocInfoE loc_174 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_174 ((LocInfoE loc_175 (use{void*} (LocInfoE loc_177 (!{void*} (LocInfoE loc_178 ("l")))))) ={PtrOp, PtrOp} (LocInfoE loc_179 (NULL))))))
569
570
571
572
573
      ]> $
    )%E
  |}.

  (* Definition of function [push]. *)
574
  Definition impl_push (global_alloc : loc): function := {|
575
    f_args := [
576
577
      ("p", void*);
      ("e", void*)
578
579
    ];
    f_local_vars := [
580
      ("node", void*)
581
582
583
584
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
585
        "node" <-{ void* }
586
          LocInfoE loc_198 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_198 (Call (LocInfoE loc_200 (global_alloc)) [@{expr} LocInfoE loc_201 (i2v (layout_of struct_list).(ly_size) size_t) ]))) ;
587
        locinfo: loc_183 ;
588
589
        LocInfoE loc_193 ((LocInfoE loc_194 (!{void*} (LocInfoE loc_195 ("node")))) at{struct_list} "head") <-{ void* }
          LocInfoE loc_196 (use{void*} (LocInfoE loc_197 ("e"))) ;
590
        locinfo: loc_184 ;
591
592
        LocInfoE loc_188 ((LocInfoE loc_189 (!{void*} (LocInfoE loc_190 ("node")))) at{struct_list} "tail") <-{ void* }
          LocInfoE loc_191 (use{void*} (LocInfoE loc_192 ("p"))) ;
593
        locinfo: loc_185 ;
594
        Return (LocInfoE loc_186 (use{void*} (LocInfoE loc_187 ("node"))))
595
596
597
598
599
      ]> $
    )%E
  |}.

  (* Definition of function [pop]. *)
600
  Definition impl_pop (global_free : loc): function := {|
601
    f_args := [
602
      ("p", void*)
603
604
    ];
    f_local_vars := [
605
606
      ("node", void*);
      ("ret", void*)
607
608
609
610
611
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
        locinfo: loc_242 ;
612
        if: LocInfoE loc_242 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_242 ((LocInfoE loc_243 (use{void*} (LocInfoE loc_245 (!{void*} (LocInfoE loc_246 ("p")))))) ={PtrOp, PtrOp} (LocInfoE loc_247 (NULL)))))
613
614
615
616
617
618
619
        then
        locinfo: loc_239 ;
          Goto "#2"
        else
        Goto "#3"
      ]> $
      <[ "#1" :=
620
621
622
623
        "node" <-{ void* }
          LocInfoE loc_232 (use{void*} (LocInfoE loc_234 (!{void*} (LocInfoE loc_235 ("p"))))) ;
        "ret" <-{ void* }
          LocInfoE loc_226 (use{void*} (LocInfoE loc_227 ((LocInfoE loc_228 (!{void*} (LocInfoE loc_229 ("node")))) at{struct_list} "head"))) ;
624
        locinfo: loc_209 ;
625
626
        LocInfoE loc_220 (!{void*} (LocInfoE loc_221 ("p"))) <-{ void* }
          LocInfoE loc_222 (use{void*} (LocInfoE loc_223 ((LocInfoE loc_224 (!{void*} (LocInfoE loc_225 ("node")))) at{struct_list} "tail"))) ;
627
        locinfo: loc_210 ;
628
629
        expr: (LocInfoE loc_210 (Call (LocInfoE loc_215 (global_free)) [@{expr} LocInfoE loc_216 (i2v (layout_of struct_list).(ly_size) size_t) ;
        LocInfoE loc_217 (use{void*} (LocInfoE loc_218 ("node"))) ])) ;
630
        locinfo: loc_211 ;
631
        Return (LocInfoE loc_212 (use{void*} (LocInfoE loc_213 ("ret"))))
632
633
634
635
636
637
638
639
640
641
642
643
644
645
      ]> $
      <[ "#2" :=
        locinfo: loc_239 ;
        Return (LocInfoE loc_240 (NULL))
      ]> $
      <[ "#3" :=
        Goto "#1"
      ]> $
    )%E
  |}.

  (* Definition of function [reverse]. *)
  Definition impl_reverse : function := {|
    f_args := [
646
      ("p", void*)
647
648
    ];
    f_local_vars := [
649
650
      ("w", void*);
      ("t", void*)
651
652
653
654
655
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
        locinfo: loc_250 ;
656
        LocInfoE loc_283 ("w") <-{ void* } LocInfoE loc_284 (NULL) ;
657
658
659
660
661
        locinfo: loc_251 ;
        Goto "#1"
      ]> $
      <[ "#1" :=
        locinfo: loc_279 ;
662
        if: LocInfoE loc_279 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_279 ((LocInfoE loc_280 (use{void*} (LocInfoE loc_281 ("p")))) !={PtrOp, PtrOp} (LocInfoE loc_282 (NULL)))))
663
664
665
666
667
668
669
670
671
        then
        locinfo: loc_257 ;
          Goto "#2"
        else
        locinfo: loc_252 ;
          Goto "#3"
      ]> $
      <[ "#2" :=
        locinfo: loc_257 ;
672
673
        LocInfoE loc_274 ("t") <-{ void* }
          LocInfoE loc_275 (use{void*} (LocInfoE loc_276 ((LocInfoE loc_277 (!{void*} (LocInfoE loc_278 ("p")))) at{struct_list} "tail"))) ;
674
        locinfo: loc_258 ;
675
676
        LocInfoE loc_269 ((LocInfoE loc_270 (!{void*} (LocInfoE loc_271 ("p")))) at{struct_list} "tail") <-{ void* }
          LocInfoE loc_272 (use{void*} (LocInfoE loc_273 ("w"))) ;
677
        locinfo: loc_259 ;
678
679
        LocInfoE loc_266 ("w") <-{ void* }
          LocInfoE loc_267 (use{void*} (LocInfoE loc_268 ("p"))) ;
680
        locinfo: loc_260 ;
681
682
        LocInfoE loc_263 ("p") <-{ void* }
          LocInfoE loc_264 (use{void*} (LocInfoE loc_265 ("t"))) ;
683
684
685
686
687
        locinfo: loc_261 ;
        Goto "continue11"
      ]> $
      <[ "#3" :=
        locinfo: loc_252 ;
688
        Return (LocInfoE loc_253 (use{void*} (LocInfoE loc_254 ("w"))))
689
690
691
692
693
694
695
696
      ]> $
      <[ "continue11" :=
        locinfo: loc_251 ;
        Goto "#1"
      ]> $
    )%E
  |}.

697
698
699
  (* Definition of function [length]. *)
  Definition impl_length : function := {|
    f_args := [
700
      ("p", void*)
701
702
703
704
705
706
707
708
709
710
711
712
713
714
    ];
    f_local_vars := [
      ("len", it_layout size_t)
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
        "len" <-{ it_layout size_t }
          LocInfoE loc_316 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_316 (i2v 0 i32))) ;
        locinfo: loc_288 ;
        Goto "#1"
      ]> $
      <[ "#1" :=
        locinfo: loc_310 ;
715
        if: LocInfoE loc_310 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_310 ((LocInfoE loc_311 (use{void*} (LocInfoE loc_313 (!{void*} (LocInfoE loc_314 ("p")))))) !={PtrOp, PtrOp} (LocInfoE loc_315 (NULL)))))
716
717
718
719
720
721
722
723
724
        then
        locinfo: loc_294 ;
          Goto "#2"
        else
        locinfo: loc_289 ;
          Goto "#3"
      ]> $
      <[ "#2" :=
        locinfo: loc_294 ;
725
726
        LocInfoE loc_303 ("p") <-{ void* }
          LocInfoE loc_304 (&(LocInfoE loc_305 ((LocInfoE loc_306 (!{void*} (LocInfoE loc_308 (!{void*} (LocInfoE loc_309 ("p")))))) at{struct_list} "tail"))) ;
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
        locinfo: loc_295 ;
        LocInfoE loc_298 ("len") <-{ it_layout size_t }
          LocInfoE loc_299 ((LocInfoE loc_300 (use{it_layout size_t} (LocInfoE loc_301 ("len")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_302 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_302 (i2v 1 i32))))) ;
        locinfo: loc_296 ;
        Goto "continue15"
      ]> $
      <[ "#3" :=
        locinfo: loc_289 ;
        Return (LocInfoE loc_290 (use{it_layout size_t} (LocInfoE loc_291 ("len"))))
      ]> $
      <[ "continue15" :=
        locinfo: loc_288 ;
        Goto "#1"
      ]> $
    )%E
  |}.

744
745
746
  (* Definition of function [length_val_rec]. *)
  Definition impl_length_val_rec (global_length_val_rec : loc): function := {|
    f_args := [
747
      ("p", void*)
748
749
750
751
752
753
754
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
        locinfo: loc_336 ;
755
        if: LocInfoE loc_336 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_336 ((LocInfoE loc_337 (use{void*} (LocInfoE loc_338 ("p")))) ={PtrOp, PtrOp} (LocInfoE loc_339 (NULL)))))
756
757
758
759
        then
        locinfo: loc_333 ;
          Goto "#2"
        else
760
        locinfo: loc_322 ;
761
762
763
764
          Goto "#3"
      ]> $
      <[ "#1" :=
        locinfo: loc_322 ;
765
        Return (LocInfoE loc_323 ((LocInfoE loc_324 (Call (LocInfoE loc_326 (global_length_val_rec)) [@{expr} LocInfoE loc_327 (use{void*} (LocInfoE loc_328 ((LocInfoE loc_329 (!{void*} (LocInfoE loc_330 ("p")))) at{struct_list} "tail"))) ])) +{IntOp size_t, IntOp size_t} (LocInfoE loc_331 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_331 (i2v 1 i32))))))
766
767
768
769
770
771
      ]> $
      <[ "#2" :=
        locinfo: loc_333 ;
        Return (LocInfoE loc_334 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_334 (i2v 0 i32))))
      ]> $
      <[ "#3" :=
772
        locinfo: loc_322 ;
773
774
775
776
777
        Goto "#1"
      ]> $
    )%E
  |}.

778
779
780
  (* Definition of function [length_val]. *)
  Definition impl_length_val : function := {|
    f_args := [
781
      ("p", void*)
782
783
784
785
786
787
788
789
790
791
792
793
794
795
    ];
    f_local_vars := [
      ("len", it_layout size_t)
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
        "len" <-{ it_layout size_t }
          LocInfoE loc_367 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_367 (i2v 0 i32))) ;
        locinfo: loc_343 ;
        Goto "#1"
      ]> $
      <[ "#1" :=
        locinfo: loc_363 ;
796
        if: LocInfoE loc_363 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_363 ((LocInfoE loc_364 (use{void*} (LocInfoE loc_365 ("p")))) !={PtrOp, PtrOp} (LocInfoE loc_366 (NULL)))))
797
798
799
800
801
802
803
804
805
        then
        locinfo: loc_349 ;
          Goto "#2"
        else
        locinfo: loc_344 ;
          Goto "#3"
      ]> $
      <[ "#2" :=
        locinfo: loc_349 ;
806
807
        LocInfoE loc_358 ("p") <-{ void* }
          LocInfoE loc_359 (use{void*} (LocInfoE loc_360 ((LocInfoE loc_361 (!{void*} (LocInfoE loc_362 ("p")))) at{struct_list} "tail"))) ;
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
        locinfo: loc_350 ;
        LocInfoE loc_353 ("len") <-{ it_layout size_t }
          LocInfoE loc_354 ((LocInfoE loc_355 (use{it_layout size_t} (LocInfoE loc_356 ("len")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_357 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_357 (i2v 1 i32))))) ;
        locinfo: loc_351 ;
        Goto "continue22"
      ]> $
      <[ "#3" :=
        locinfo: loc_344 ;
        Return (LocInfoE loc_345 (use{it_layout size_t} (LocInfoE loc_346 ("len"))))
      ]> $
      <[ "continue22" :=
        locinfo: loc_343 ;
        Goto "#1"
      ]> $
    )%E
  |}.

825
826
827
  (* Definition of function [append]. *)
  Definition impl_append : function := {|
    f_args := [
828
829
      ("l1", void*);
      ("l2", void*)
830
831
    ];
    f_local_vars := [
832
      ("end", void*)
833
834
835
836
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
837
838
        "end" <-{ void* }
          LocInfoE loc_398 (use{void*} (LocInfoE loc_399 ("l1"))) ;
839
        locinfo: loc_373 ;
840
841
842
        Goto "#1"
      ]> $
      <[ "#1" :=
843
        locinfo: loc_392 ;
844
        if: LocInfoE loc_392 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_392 ((LocInfoE loc_393 (use{void*} (LocInfoE loc_395 (!{void*} (LocInfoE loc_396 ("end")))))) !={PtrOp, PtrOp} (LocInfoE loc_397 (NULL)))))
845
        then
846
        locinfo: loc_382 ;
847
848
          Goto "#2"
        else
849
        locinfo: loc_374 ;
850
851
852
          Goto "#3"
      ]> $
      <[ "#2" :=
853
        locinfo: loc_382 ;
854
855
        LocInfoE loc_385 ("end") <-{ void* }
          LocInfoE loc_386 (&(LocInfoE loc_387 ((LocInfoE loc_388 (!{void*} (LocInfoE loc_390 (!{void*} (LocInfoE loc_391 ("end")))))) at{struct_list} "tail"))) ;
856
857
        locinfo: loc_383 ;
        Goto "continue26"
858
859
      ]> $
      <[ "#3" :=
860
        locinfo: loc_374 ;
861
862
        LocInfoE loc_376 (!{void*} (LocInfoE loc_377 ("end"))) <-{ void* }
          LocInfoE loc_378 (use{void*} (LocInfoE loc_379 ("l2"))) ;
863
864
        Return (VOID)
      ]> $
865
866
      <[ "continue26" :=
        locinfo: loc_373 ;
867
868
869
870
871
872
873
874
        Goto "#1"
      ]> $
    )%E
  |}.

  (* Definition of function [member]. *)
  Definition impl_member : function := {|
    f_args := [
875
      ("p", void*);
876
877
878
      ("k", it_layout size_t)
    ];
    f_local_vars := [
879
880
881
      ("prev", void*);
      ("cur", void*);
      ("head", void*)
882
883
884
885
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
886
887
        "prev" <-{ void* }
          LocInfoE loc_450 (use{void*} (LocInfoE loc_451 ("p"))) ;
888
        locinfo: loc_405 ;
889
890
891
        Goto "#1"
      ]> $
      <[ "#1" :=
892
        locinfo: loc_444 ;
893
        if: LocInfoE loc_444 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_444 ((LocInfoE loc_445 (use{void*} (LocInfoE loc_447 (!{void*} (LocInfoE loc_448 ("prev")))))) !={PtrOp, PtrOp} (LocInfoE loc_449 (NULL)))))
894
895
896
        then
        Goto "#2"
        else
897
        locinfo: loc_406 ;
898
899
900
          Goto "#3"
      ]> $
      <[ "#2" :=
901
902
903
904
        "cur" <-{ void* }
          LocInfoE loc_438 (use{void*} (LocInfoE loc_440 (!{void*} (LocInfoE loc_441 ("prev"))))) ;
        "head" <-{ void* }
          LocInfoE loc_432 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_432 (use{void*} (LocInfoE loc_433 ((LocInfoE loc_434 (!{void*} (LocInfoE loc_435 ("cur")))) at{struct_list} "head"))))) ;
905
        locinfo: loc_425 ;
906
        if: LocInfoE loc_425 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_425 ((LocInfoE loc_426 (use{it_layout size_t} (LocInfoE loc_428 (!{void*} (LocInfoE loc_429 ("head")))))) ={IntOp size_t, IntOp size_t} (LocInfoE loc_430 (use{it_layout size_t} (LocInfoE loc_431 ("k")))))))
907
        then
908
        locinfo: loc_422 ;
909
910
          Goto "#5"
        else
911
        locinfo: loc_413 ;
912
913
914
          Goto "#6"
      ]> $
      <[ "#3" :=
915
916
        locinfo: loc_406 ;
        Return (LocInfoE loc_407 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_407 (i2v 0 i32))))
917
918
      ]> $
      <[ "#4" :=
919
        locinfo: loc_413 ;
920
921
        LocInfoE loc_416 ("prev") <-{ void* }
          LocInfoE loc_417 (&(LocInfoE loc_418 ((LocInfoE loc_419 (!{void*} (LocInfoE loc_420 ("cur")))) at{struct_list} "tail"))) ;
922
923
        locinfo: loc_414 ;
        Goto "continue30"
924
925
      ]> $
      <[ "#5" :=
926
927
        locinfo: loc_422 ;
        Return (LocInfoE loc_423 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_423 (i2v 1 i32))))
928
929
      ]> $
      <[ "#6" :=
930
        locinfo: loc_413 ;
931
932
        Goto "#4"
      ]> $
933
934
      <[ "continue30" :=
        locinfo: loc_405 ;
935
936
937
938
939
940
941
942
        Goto "#1"
      ]> $
    )%E
  |}.

  (* Definition of function [rev_append]. *)
  Definition impl_rev_append : function := {|
    f_args := [
943
944
      ("l1", void*);
      ("l2", void*)
945
946
    ];
    f_local_vars := [
947
948
      ("cur", void*);
      ("cur_tail", void*)
949
950
951
952
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
953
954
        "cur" <-{ void* }
          LocInfoE loc_490 (use{void*} (LocInfoE loc_491 ("l1"))) ;
955
        locinfo: loc_457 ;
956
957
958
        Goto "#1"
      ]> $
      <[ "#1" :=
959
        locinfo: loc_486 ;
960
        if: LocInfoE loc_486 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_486 ((LocInfoE loc_487 (use{void*} (LocInfoE loc_488 ("cur")))) !={PtrOp, PtrOp} (LocInfoE loc_489 (NULL)))))
961
        then
962
        locinfo: loc_460 ;
963
964
965
966
967
          Goto "#2"
        else
        Goto "#3"
      ]> $
      <[ "#2" :=
968
        locinfo: loc_460 ;
969
970
        LocInfoE loc_481 ("cur_tail") <-{ void* }
          LocInfoE loc_482 (use{void*} (LocInfoE loc_483 ((LocInfoE loc_484 (!{void*} (LocInfoE loc_485 ("cur")))) at{struct_list} "tail"))) ;
971
        locinfo: loc_461 ;
972
973
        LocInfoE loc_474 ((LocInfoE loc_475 (!{void*} (LocInfoE loc_476 ("cur")))) at{struct_list} "tail") <-{ void* }
          LocInfoE loc_477 (use{void*} (LocInfoE loc_479 (!{void*} (LocInfoE loc_480 ("l2"))))) ;
974
        locinfo: loc_462 ;
975
976
        LocInfoE loc_470 (!{void*} (LocInfoE loc_471 ("l2"))) <-{ void* }
          LocInfoE loc_472 (use{void*} (LocInfoE loc_473 ("cur"))) ;
977
        locinfo: loc_463 ;
978
979
        LocInfoE loc_466 ("cur") <-{ void* }
          LocInfoE loc_467 (use{void*} (LocInfoE loc_468 ("cur_tail"))) ;
980
981
        locinfo: loc_464 ;
        Goto "continue37"
982
983
984
985
      ]> $
      <[ "#3" :=
        Return (VOID)
      ]> $
986
987
      <[ "continue37" :=
        locinfo: loc_457 ;
988
989
990
991
992
        Goto "#1"
      ]> $
    )%E
  |}.
End code.