generated_code.v 108 KB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1
2
3
4
5
6
7
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 [linux/casestudies/page_alloc.c]. *)
Section code.
8
  Definition file_0 : string := "include/refinedc.h".
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
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
276
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
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
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
  Definition file_1 : string := "linux/casestudies/page_alloc.c".
  Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
  Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.
  Definition loc_4 : location_info := LocationInfo file_0 49 9 49 32.
  Definition loc_5 : location_info := LocationInfo file_0 49 33 49 37.
  Definition loc_6 : location_info := LocationInfo file_0 49 33 49 37.
  Definition loc_7 : location_info := LocationInfo file_0 49 39 49 45.
  Definition loc_8 : location_info := LocationInfo file_0 49 39 49 45.
  Definition loc_11 : location_info := LocationInfo file_1 34 1 34 11.
  Definition loc_12 : location_info := LocationInfo file_1 34 8 34 9.
  Definition loc_15 : location_info := LocationInfo file_1 64 1 64 10.
  Definition loc_16 : location_info := LocationInfo file_1 64 8 64 9.
  Definition loc_19 : location_info := LocationInfo file_1 68 1 68 10.
  Definition loc_20 : location_info := LocationInfo file_1 68 8 68 9.
  Definition loc_23 : location_info := LocationInfo file_1 80 1 80 25.
  Definition loc_24 : location_info := LocationInfo file_1 81 1 81 19.
  Definition loc_25 : location_info := LocationInfo file_1 81 1 81 11.
  Definition loc_26 : location_info := LocationInfo file_1 81 1 81 5.
  Definition loc_27 : location_info := LocationInfo file_1 81 1 81 5.
  Definition loc_28 : location_info := LocationInfo file_1 81 14 81 18.
  Definition loc_29 : location_info := LocationInfo file_1 81 14 81 18.
  Definition loc_30 : location_info := LocationInfo file_1 80 2 80 14.
  Definition loc_31 : location_info := LocationInfo file_1 80 3 80 7.
  Definition loc_32 : location_info := LocationInfo file_1 80 3 80 7.
  Definition loc_33 : location_info := LocationInfo file_1 80 17 80 23.
  Definition loc_34 : location_info := LocationInfo file_1 80 17 80 23.
  Definition loc_37 : location_info := LocationInfo file_1 94 1 95 9.
  Definition loc_38 : location_info := LocationInfo file_1 97 1 97 18.
  Definition loc_39 : location_info := LocationInfo file_1 98 1 98 18.
  Definition loc_40 : location_info := LocationInfo file_1 99 1 99 18.
  Definition loc_41 : location_info := LocationInfo file_1 100 1 100 24.
  Definition loc_42 : location_info := LocationInfo file_1 100 2 100 14.
  Definition loc_43 : location_info := LocationInfo file_1 100 3 100 7.
  Definition loc_44 : location_info := LocationInfo file_1 100 3 100 7.
  Definition loc_45 : location_info := LocationInfo file_1 100 17 100 22.
  Definition loc_46 : location_info := LocationInfo file_1 100 17 100 22.
  Definition loc_47 : location_info := LocationInfo file_1 99 1 99 10.
  Definition loc_48 : location_info := LocationInfo file_1 99 1 99 4.
  Definition loc_49 : location_info := LocationInfo file_1 99 1 99 4.
  Definition loc_50 : location_info := LocationInfo file_1 99 13 99 17.
  Definition loc_51 : location_info := LocationInfo file_1 99 13 99 17.
  Definition loc_52 : location_info := LocationInfo file_1 98 1 98 10.
  Definition loc_53 : location_info := LocationInfo file_1 98 1 98 4.
  Definition loc_54 : location_info := LocationInfo file_1 98 1 98 4.
  Definition loc_55 : location_info := LocationInfo file_1 98 13 98 17.
  Definition loc_56 : location_info := LocationInfo file_1 98 13 98 17.
  Definition loc_57 : location_info := LocationInfo file_1 97 1 97 11.
  Definition loc_58 : location_info := LocationInfo file_1 97 1 97 5.
  Definition loc_59 : location_info := LocationInfo file_1 97 1 97 5.
  Definition loc_60 : location_info := LocationInfo file_1 97 14 97 17.
  Definition loc_61 : location_info := LocationInfo file_1 97 14 97 17.
  Definition loc_62 : location_info := LocationInfo file_1 95 2 95 9.
  Definition loc_65 : location_info := LocationInfo file_1 94 5 94 39.
  Definition loc_67 : location_info := LocationInfo file_1 94 6 94 39.
  Definition loc_68 : location_info := LocationInfo file_1 94 6 94 22.
  Definition loc_69 : location_info := LocationInfo file_1 94 6 94 22.
  Definition loc_70 : location_info := LocationInfo file_1 94 23 94 26.
  Definition loc_71 : location_info := LocationInfo file_1 94 23 94 26.
  Definition loc_72 : location_info := LocationInfo file_1 94 28 94 32.
  Definition loc_73 : location_info := LocationInfo file_1 94 28 94 32.
  Definition loc_74 : location_info := LocationInfo file_1 94 34 94 38.
  Definition loc_75 : location_info := LocationInfo file_1 94 34 94 38.
  Definition loc_78 : location_info := LocationInfo file_1 117 1 117 35.
  Definition loc_79 : location_info := LocationInfo file_1 117 1 117 11.
  Definition loc_80 : location_info := LocationInfo file_1 117 1 117 11.
  Definition loc_81 : location_info := LocationInfo file_1 117 12 117 15.
  Definition loc_82 : location_info := LocationInfo file_1 117 12 117 15.
  Definition loc_83 : location_info := LocationInfo file_1 117 17 117 21.
  Definition loc_84 : location_info := LocationInfo file_1 117 17 117 21.
  Definition loc_85 : location_info := LocationInfo file_1 117 23 117 33.
  Definition loc_86 : location_info := LocationInfo file_1 117 23 117 33.
  Definition loc_87 : location_info := LocationInfo file_1 117 23 117 27.
  Definition loc_88 : location_info := LocationInfo file_1 117 23 117 27.
  Definition loc_91 : location_info := LocationInfo file_1 131 1 131 35.
  Definition loc_92 : location_info := LocationInfo file_1 131 1 131 11.
  Definition loc_93 : location_info := LocationInfo file_1 131 1 131 11.
  Definition loc_94 : location_info := LocationInfo file_1 131 12 131 15.
  Definition loc_95 : location_info := LocationInfo file_1 131 12 131 15.
  Definition loc_96 : location_info := LocationInfo file_1 131 17 131 27.
  Definition loc_97 : location_info := LocationInfo file_1 131 17 131 27.
  Definition loc_98 : location_info := LocationInfo file_1 131 17 131 21.
  Definition loc_99 : location_info := LocationInfo file_1 131 17 131 21.
  Definition loc_100 : location_info := LocationInfo file_1 131 29 131 33.
  Definition loc_101 : location_info := LocationInfo file_1 131 29 131 33.
  Definition loc_104 : location_info := LocationInfo file_1 143 1 143 19.
  Definition loc_105 : location_info := LocationInfo file_1 144 1 144 25.
  Definition loc_106 : location_info := LocationInfo file_1 144 2 144 14.
  Definition loc_107 : location_info := LocationInfo file_1 144 3 144 7.
  Definition loc_108 : location_info := LocationInfo file_1 144 3 144 7.
  Definition loc_109 : location_info := LocationInfo file_1 144 17 144 23.
  Definition loc_110 : location_info := LocationInfo file_1 144 17 144 23.
  Definition loc_111 : location_info := LocationInfo file_1 143 1 143 11.
  Definition loc_112 : location_info := LocationInfo file_1 143 1 143 5.
  Definition loc_113 : location_info := LocationInfo file_1 143 1 143 5.
  Definition loc_114 : location_info := LocationInfo file_1 143 14 143 18.
  Definition loc_115 : location_info := LocationInfo file_1 143 14 143 18.
  Definition loc_118 : location_info := LocationInfo file_1 149 1 150 9.
  Definition loc_119 : location_info := LocationInfo file_1 152 1 152 38.
  Definition loc_120 : location_info := LocationInfo file_1 152 1 152 11.
  Definition loc_121 : location_info := LocationInfo file_1 152 1 152 11.
  Definition loc_122 : location_info := LocationInfo file_1 152 12 152 23.
  Definition loc_123 : location_info := LocationInfo file_1 152 12 152 23.
  Definition loc_124 : location_info := LocationInfo file_1 152 12 152 17.
  Definition loc_125 : location_info := LocationInfo file_1 152 12 152 17.
  Definition loc_126 : location_info := LocationInfo file_1 152 25 152 36.
  Definition loc_127 : location_info := LocationInfo file_1 152 25 152 36.
  Definition loc_128 : location_info := LocationInfo file_1 152 25 152 30.
  Definition loc_129 : location_info := LocationInfo file_1 152 25 152 30.
  Definition loc_130 : location_info := LocationInfo file_1 150 2 150 9.
  Definition loc_133 : location_info := LocationInfo file_1 149 5 149 35.
  Definition loc_135 : location_info := LocationInfo file_1 149 6 149 35.
  Definition loc_136 : location_info := LocationInfo file_1 149 6 149 28.
  Definition loc_137 : location_info := LocationInfo file_1 149 6 149 28.
  Definition loc_138 : location_info := LocationInfo file_1 149 29 149 34.
  Definition loc_139 : location_info := LocationInfo file_1 149 29 149 34.
  Definition loc_142 : location_info := LocationInfo file_1 166 1 166 25.
  Definition loc_143 : location_info := LocationInfo file_1 167 1 167 23.
  Definition loc_144 : location_info := LocationInfo file_1 167 1 167 15.
  Definition loc_145 : location_info := LocationInfo file_1 167 1 167 15.
  Definition loc_146 : location_info := LocationInfo file_1 167 16 167 21.
  Definition loc_147 : location_info := LocationInfo file_1 167 16 167 21.
  Definition loc_148 : location_info := LocationInfo file_1 166 1 166 17.
  Definition loc_149 : location_info := LocationInfo file_1 166 1 166 17.
  Definition loc_150 : location_info := LocationInfo file_1 166 18 166 23.
  Definition loc_151 : location_info := LocationInfo file_1 166 18 166 23.
  Definition loc_154 : location_info := LocationInfo file_1 181 1 181 29.
  Definition loc_155 : location_info := LocationInfo file_1 181 8 181 28.
  Definition loc_156 : location_info := LocationInfo file_1 181 8 181 20.
  Definition loc_157 : location_info := LocationInfo file_1 181 8 181 20.
  Definition loc_158 : location_info := LocationInfo file_1 181 9 181 13.
  Definition loc_159 : location_info := LocationInfo file_1 181 9 181 13.
  Definition loc_160 : location_info := LocationInfo file_1 181 24 181 28.
  Definition loc_161 : location_info := LocationInfo file_1 181 24 181 28.
  Definition loc_164 : location_info := LocationInfo file_1 248 1 248 62.
  Definition loc_165 : location_info := LocationInfo file_1 248 8 248 61.
  Definition loc_166 : location_info := LocationInfo file_1 248 17 248 60.
  Definition loc_167 : location_info := LocationInfo file_1 248 18 248 37.
  Definition loc_168 : location_info := LocationInfo file_1 248 31 248 37.
  Definition loc_169 : location_info := LocationInfo file_1 248 31 248 37.
  Definition loc_170 : location_info := LocationInfo file_1 248 40 248 59.
  Definition loc_171 : location_info := LocationInfo file_1 248 40 248 59.
  Definition loc_174 : location_info := LocationInfo file_1 253 1 253 52.
  Definition loc_175 : location_info := LocationInfo file_1 253 8 253 51.
  Definition loc_176 : location_info := LocationInfo file_1 253 9 253 28.
  Definition loc_177 : location_info := LocationInfo file_1 253 22 253 28.
  Definition loc_178 : location_info := LocationInfo file_1 253 22 253 28.
  Definition loc_179 : location_info := LocationInfo file_1 253 31 253 50.
  Definition loc_180 : location_info := LocationInfo file_1 253 31 253 50.
  Definition loc_183 : location_info := LocationInfo file_1 266 1 266 62.
  Definition loc_184 : location_info := LocationInfo file_1 266 8 266 61.
  Definition loc_185 : location_info := LocationInfo file_1 266 9 266 43.
  Definition loc_186 : location_info := LocationInfo file_1 266 29 266 42.
  Definition loc_187 : location_info := LocationInfo file_1 266 29 266 42.
  Definition loc_188 : location_info := LocationInfo file_1 266 46 266 60.
  Definition loc_189 : location_info := LocationInfo file_1 266 47 266 53.
  Definition loc_190 : location_info := LocationInfo file_1 266 47 266 53.
  Definition loc_191 : location_info := LocationInfo file_1 266 57 266 59.
  Definition loc_194 : location_info := LocationInfo file_1 278 1 278 75.
  Definition loc_195 : location_info := LocationInfo file_1 278 8 278 74.
  Definition loc_196 : location_info := LocationInfo file_1 278 9 278 67.
  Definition loc_197 : location_info := LocationInfo file_1 278 22 278 67.
  Definition loc_198 : location_info := LocationInfo file_1 278 23 278 29.
  Definition loc_199 : location_info := LocationInfo file_1 278 23 278 29.
  Definition loc_200 : location_info := LocationInfo file_1 278 32 278 66.
  Definition loc_201 : location_info := LocationInfo file_1 278 52 278 65.
  Definition loc_202 : location_info := LocationInfo file_1 278 52 278 65.
  Definition loc_203 : location_info := LocationInfo file_1 278 71 278 73.
  Definition loc_206 : location_info := LocationInfo file_1 285 1 285 84.
  Definition loc_207 : location_info := LocationInfo file_1 287 1 287 20.
  Definition loc_208 : location_info := LocationInfo file_1 287 8 287 19.
  Definition loc_209 : location_info := LocationInfo file_1 287 8 287 19.
  Definition loc_210 : location_info := LocationInfo file_1 287 8 287 9.
  Definition loc_211 : location_info := LocationInfo file_1 287 8 287 9.
  Definition loc_212 : location_info := LocationInfo file_1 285 22 285 83.
  Definition loc_213 : location_info := LocationInfo file_1 285 22 285 38.
  Definition loc_214 : location_info := LocationInfo file_1 285 22 285 38.
  Definition loc_215 : location_info := LocationInfo file_1 285 39 285 82.
  Definition loc_216 : location_info := LocationInfo file_1 285 40 285 59.
  Definition loc_217 : location_info := LocationInfo file_1 285 53 285 59.
  Definition loc_218 : location_info := LocationInfo file_1 285 53 285 59.
  Definition loc_219 : location_info := LocationInfo file_1 285 62 285 81.
  Definition loc_220 : location_info := LocationInfo file_1 285 62 285 81.
  Definition loc_225 : location_info := LocationInfo file_1 522 1 522 22.
  Definition loc_226 : location_info := LocationInfo file_1 523 1 523 42.
  Definition loc_227 : location_info := LocationInfo file_1 524 1 524 24.
  Definition loc_228 : location_info := LocationInfo file_1 526 1 526 98.
  Definition loc_229 : location_info := LocationInfo file_1 526 8 526 97.
  Definition loc_230 : location_info := LocationInfo file_1 526 8 526 9.
  Definition loc_231 : location_info := LocationInfo file_1 526 8 526 9.
  Definition loc_232 : location_info := LocationInfo file_1 526 12 526 80.
  Definition loc_233 : location_info := LocationInfo file_1 526 21 526 79.
  Definition loc_234 : location_info := LocationInfo file_1 526 22 526 56.
  Definition loc_235 : location_info := LocationInfo file_1 526 35 526 56.
  Definition loc_236 : location_info := LocationInfo file_1 526 36 526 52.
  Definition loc_237 : location_info := LocationInfo file_1 526 36 526 52.
  Definition loc_238 : location_info := LocationInfo file_1 526 53 526 54.
  Definition loc_239 : location_info := LocationInfo file_1 526 53 526 54.
  Definition loc_240 : location_info := LocationInfo file_1 526 59 526 78.
  Definition loc_241 : location_info := LocationInfo file_1 526 59 526 78.
  Definition loc_242 : location_info := LocationInfo file_1 526 83 526 97.
  Definition loc_243 : location_info := LocationInfo file_1 524 1 524 10.
  Definition loc_244 : location_info := LocationInfo file_1 524 1 524 10.
  Definition loc_245 : location_info := LocationInfo file_1 524 11 524 22.
  Definition loc_246 : location_info := LocationInfo file_1 524 12 524 22.
  Definition loc_247 : location_info := LocationInfo file_1 524 12 524 16.
  Definition loc_248 : location_info := LocationInfo file_1 524 12 524 16.
  Definition loc_249 : location_info := LocationInfo file_1 523 1 523 2.
  Definition loc_250 : location_info := LocationInfo file_1 523 5 523 41.
  Definition loc_251 : location_info := LocationInfo file_1 523 5 523 22.
  Definition loc_252 : location_info := LocationInfo file_1 523 5 523 22.
  Definition loc_253 : location_info := LocationInfo file_1 523 23 523 27.
  Definition loc_254 : location_info := LocationInfo file_1 523 23 523 27.
  Definition loc_255 : location_info := LocationInfo file_1 523 29 523 33.
  Definition loc_256 : location_info := LocationInfo file_1 523 29 523 33.
  Definition loc_257 : location_info := LocationInfo file_1 523 35 523 40.
  Definition loc_258 : location_info := LocationInfo file_1 523 35 523 40.
  Definition loc_259 : location_info := LocationInfo file_1 522 1 522 8.
  Definition loc_260 : location_info := LocationInfo file_1 522 1 522 8.
  Definition loc_261 : location_info := LocationInfo file_1 522 9 522 20.
  Definition loc_262 : location_info := LocationInfo file_1 522 10 522 20.
  Definition loc_263 : location_info := LocationInfo file_1 522 10 522 14.
  Definition loc_264 : location_info := LocationInfo file_1 522 10 522 14.
  Definition loc_267 : location_info := LocationInfo file_1 453 1 453 84.
  Definition loc_268 : location_info := LocationInfo file_1 454 1 454 56.
  Definition loc_269 : location_info := LocationInfo file_1 456 1 456 22.
  Definition loc_270 : location_info := LocationInfo file_1 457 1 457 15.
  Definition loc_271 : location_info := LocationInfo file_1 458 1 458 24.
  Definition loc_272 : location_info := LocationInfo file_1 458 1 458 10.
  Definition loc_273 : location_info := LocationInfo file_1 458 1 458 10.
  Definition loc_274 : location_info := LocationInfo file_1 458 11 458 22.
  Definition loc_275 : location_info := LocationInfo file_1 458 12 458 22.
  Definition loc_276 : location_info := LocationInfo file_1 458 12 458 16.
  Definition loc_277 : location_info := LocationInfo file_1 458 12 458 16.
  Definition loc_278 : location_info := LocationInfo file_1 457 1 457 12.
  Definition loc_279 : location_info := LocationInfo file_1 457 1 457 2.
  Definition loc_280 : location_info := LocationInfo file_1 457 1 457 2.
  Definition loc_281 : location_info := LocationInfo file_1 456 1 456 8.
  Definition loc_282 : location_info := LocationInfo file_1 456 1 456 8.
  Definition loc_283 : location_info := LocationInfo file_1 456 9 456 20.
  Definition loc_284 : location_info := LocationInfo file_1 456 10 456 20.
  Definition loc_285 : location_info := LocationInfo file_1 456 10 456 14.
  Definition loc_286 : location_info := LocationInfo file_1 456 10 456 14.
  Definition loc_287 : location_info := LocationInfo file_1 454 25 454 55.
  Definition loc_288 : location_info := LocationInfo file_1 454 25 454 55.
  Definition loc_289 : location_info := LocationInfo file_1 454 26 454 48.
  Definition loc_290 : location_info := LocationInfo file_1 454 46 454 47.
  Definition loc_291 : location_info := LocationInfo file_1 454 46 454 47.
  Definition loc_294 : location_info := LocationInfo file_1 453 22 453 83.
  Definition loc_295 : location_info := LocationInfo file_1 453 22 453 38.
  Definition loc_296 : location_info := LocationInfo file_1 453 22 453 38.
  Definition loc_297 : location_info := LocationInfo file_1 453 39 453 82.
  Definition loc_298 : location_info := LocationInfo file_1 453 40 453 59.
  Definition loc_299 : location_info := LocationInfo file_1 453 53 453 59.
  Definition loc_300 : location_info := LocationInfo file_1 453 53 453 59.
  Definition loc_301 : location_info := LocationInfo file_1 453 62 453 81.
  Definition loc_302 : location_info := LocationInfo file_1 453 62 453 81.
  Definition loc_307 : location_info := LocationInfo file_1 439 1 439 84.
  Definition loc_308 : location_info := LocationInfo file_1 440 1 440 56.
  Definition loc_309 : location_info := LocationInfo file_1 442 1 442 22.
  Definition loc_310 : location_info := LocationInfo file_1 443 1 444 14.
  Definition loc_311 : location_info := LocationInfo file_1 445 1 445 15.
  Definition loc_312 : location_info := LocationInfo file_1 446 1 447 29.
  Definition loc_313 : location_info := LocationInfo file_1 448 1 448 24.
  Definition loc_314 : location_info := LocationInfo file_1 448 1 448 10.
  Definition loc_315 : location_info := LocationInfo file_1 448 1 448 10.
  Definition loc_316 : location_info := LocationInfo file_1 448 11 448 22.
  Definition loc_317 : location_info := LocationInfo file_1 448 12 448 22.
  Definition loc_318 : location_info := LocationInfo file_1 448 12 448 16.
  Definition loc_319 : location_info := LocationInfo file_1 448 12 448 16.
  Definition loc_320 : location_info := LocationInfo file_1 447 2 447 29.
  Definition loc_321 : location_info := LocationInfo file_1 447 2 447 19.
  Definition loc_322 : location_info := LocationInfo file_1 447 2 447 19.
  Definition loc_323 : location_info := LocationInfo file_1 447 20 447 24.
  Definition loc_324 : location_info := LocationInfo file_1 447 20 447 24.
  Definition loc_325 : location_info := LocationInfo file_1 447 26 447 27.
  Definition loc_326 : location_info := LocationInfo file_1 447 26 447 27.
  Definition loc_328 : location_info := LocationInfo file_1 446 5 446 17.
  Definition loc_330 : location_info := LocationInfo file_1 446 6 446 17.
  Definition loc_331 : location_info := LocationInfo file_1 446 6 446 17.
  Definition loc_332 : location_info := LocationInfo file_1 446 6 446 7.
  Definition loc_333 : location_info := LocationInfo file_1 446 6 446 7.
  Definition loc_334 : location_info := LocationInfo file_1 445 1 445 12.
  Definition loc_335 : location_info := LocationInfo file_1 445 1 445 2.
  Definition loc_336 : location_info := LocationInfo file_1 445 1 445 2.
  Definition loc_337 : location_info := LocationInfo file_1 444 2 444 14.
  Definition loc_338 : location_info := LocationInfo file_1 444 2 444 11.
  Definition loc_339 : location_info := LocationInfo file_1 444 2 444 11.
  Definition loc_341 : location_info := LocationInfo file_1 443 5 443 17.
  Definition loc_343 : location_info := LocationInfo file_1 443 6 443 17.
  Definition loc_344 : location_info := LocationInfo file_1 443 6 443 17.
  Definition loc_345 : location_info := LocationInfo file_1 443 6 443 7.
  Definition loc_346 : location_info := LocationInfo file_1 443 6 443 7.
  Definition loc_347 : location_info := LocationInfo file_1 442 1 442 8.
  Definition loc_348 : location_info := LocationInfo file_1 442 1 442 8.
  Definition loc_349 : location_info := LocationInfo file_1 442 9 442 20.
  Definition loc_350 : location_info := LocationInfo file_1 442 10 442 20.
  Definition loc_351 : location_info := LocationInfo file_1 442 10 442 14.
  Definition loc_352 : location_info := LocationInfo file_1 442 10 442 14.
  Definition loc_353 : location_info := LocationInfo file_1 440 25 440 55.
  Definition loc_354 : location_info := LocationInfo file_1 440 25 440 55.
  Definition loc_355 : location_info := LocationInfo file_1 440 26 440 48.
  Definition loc_356 : location_info := LocationInfo file_1 440 46 440 47.
  Definition loc_357 : location_info := LocationInfo file_1 440 46 440 47.
  Definition loc_360 : location_info := LocationInfo file_1 439 22 439 83.
  Definition loc_361 : location_info := LocationInfo file_1 439 22 439 38.
  Definition loc_362 : location_info := LocationInfo file_1 439 22 439 38.
  Definition loc_363 : location_info := LocationInfo file_1 439 39 439 82.
  Definition loc_364 : location_info := LocationInfo file_1 439 40 439 59.
  Definition loc_365 : location_info := LocationInfo file_1 439 53 439 59.
  Definition loc_366 : location_info := LocationInfo file_1 439 53 439 59.
  Definition loc_367 : location_info := LocationInfo file_1 439 62 439 81.
  Definition loc_368 : location_info := LocationInfo file_1 439 62 439 81.
  Definition loc_373 : location_info := LocationInfo file_1 536 1 537 13.
  Definition loc_374 : location_info := LocationInfo file_1 539 1 539 22.
  Definition loc_375 : location_info := LocationInfo file_1 540 6 540 11.
  Definition loc_376 : location_info := LocationInfo file_1 540 1 541 38.
  Definition loc_377 : location_info := LocationInfo file_1 542 1 542 26.
  Definition loc_378 : location_info := LocationInfo file_1 543 1 543 43.
  Definition loc_379 : location_info := LocationInfo file_1 546 1 546 28.
  Definition loc_380 : location_info := LocationInfo file_1 547 1 547 37.
  Definition loc_381 : location_info := LocationInfo file_1 550 6 550 11.
  Definition loc_382 : location_info := LocationInfo file_1 550 1 554 2.
  Definition loc_383 : location_info := LocationInfo file_1 557 1 557 49.
  Definition loc_384 : location_info := LocationInfo file_1 560 6 560 20.
  Definition loc_385 : location_info := LocationInfo file_1 560 1 563 2.
  Definition loc_386 : location_info := LocationInfo file_1 565 1 565 10.
  Definition loc_387 : location_info := LocationInfo file_1 565 8 565 9.
  Definition loc_388 : location_info := LocationInfo file_1 560 41 563 2.
  Definition loc_389 : location_info := LocationInfo file_1 561 2 561 29.
  Definition loc_390 : location_info := LocationInfo file_1 562 2 562 6.
  Definition loc_391 : location_info := LocationInfo file_1 560 1 563 2.
  Definition loc_392 : location_info := LocationInfo file_1 560 36 560 39.
  Definition loc_393 : location_info := LocationInfo file_1 560 36 560 37.
  Definition loc_394 : location_info := LocationInfo file_1 562 2 562 3.
  Definition loc_395 : location_info := LocationInfo file_1 561 2 561 19.
  Definition loc_396 : location_info := LocationInfo file_1 561 2 561 19.
  Definition loc_397 : location_info := LocationInfo file_1 561 20 561 24.
  Definition loc_398 : location_info := LocationInfo file_1 561 20 561 24.
  Definition loc_399 : location_info := LocationInfo file_1 561 26 561 27.
  Definition loc_400 : location_info := LocationInfo file_1 561 26 561 27.
  Definition loc_401 : location_info := LocationInfo file_1 560 22 560 34.
  Definition loc_402 : location_info := LocationInfo file_1 560 22 560 23.
  Definition loc_403 : location_info := LocationInfo file_1 560 22 560 23.
  Definition loc_404 : location_info := LocationInfo file_1 560 26 560 34.
  Definition loc_405 : location_info := LocationInfo file_1 560 26 560 34.
  Definition loc_406 : location_info := LocationInfo file_1 560 6 560 7.
  Definition loc_407 : location_info := LocationInfo file_1 560 10 560 20.
  Definition loc_408 : location_info := LocationInfo file_1 560 10 560 20.
  Definition loc_409 : location_info := LocationInfo file_1 557 1 557 2.
  Definition loc_410 : location_info := LocationInfo file_1 557 5 557 48.
  Definition loc_411 : location_info := LocationInfo file_1 557 5 557 21.
  Definition loc_412 : location_info := LocationInfo file_1 557 5 557 21.
  Definition loc_413 : location_info := LocationInfo file_1 557 22 557 47.
  Definition loc_414 : location_info := LocationInfo file_1 557 22 557 26.
  Definition loc_415 : location_info := LocationInfo file_1 557 22 557 26.
  Definition loc_416 : location_info := LocationInfo file_1 557 29 557 47.
  Definition loc_417 : location_info := LocationInfo file_1 557 30 557 40.
  Definition loc_418 : location_info := LocationInfo file_1 557 30 557 40.
  Definition loc_419 : location_info := LocationInfo file_1 557 44 557 46.
  Definition loc_420 : location_info := LocationInfo file_1 550 32 554 2.
  Definition loc_421 : location_info := LocationInfo file_1 551 2 551 17.
  Definition loc_422 : location_info := LocationInfo file_1 552 2 552 27.
  Definition loc_423 : location_info := LocationInfo file_1 553 2 553 6.
  Definition loc_424 : location_info := LocationInfo file_1 550 1 554 2.
  Definition loc_425 : location_info := LocationInfo file_1 550 27 550 30.
  Definition loc_426 : location_info := LocationInfo file_1 550 27 550 28.
  Definition loc_427 : location_info := LocationInfo file_1 553 2 553 3.
  Definition loc_428 : location_info := LocationInfo file_1 552 2 552 16.
  Definition loc_429 : location_info := LocationInfo file_1 552 2 552 16.
  Definition loc_430 : location_info := LocationInfo file_1 552 17 552 25.
  Definition loc_431 : location_info := LocationInfo file_1 552 18 552 25.
  Definition loc_432 : location_info := LocationInfo file_1 552 18 552 19.
  Definition loc_433 : location_info := LocationInfo file_1 552 18 552 19.
  Definition loc_434 : location_info := LocationInfo file_1 551 2 551 9.
  Definition loc_435 : location_info := LocationInfo file_1 551 2 551 3.
  Definition loc_436 : location_info := LocationInfo file_1 551 2 551 3.
  Definition loc_437 : location_info := LocationInfo file_1 551 12 551 16.
  Definition loc_438 : location_info := LocationInfo file_1 551 12 551 16.
  Definition loc_439 : location_info := LocationInfo file_1 550 13 550 25.
  Definition loc_440 : location_info := LocationInfo file_1 550 13 550 14.
  Definition loc_441 : location_info := LocationInfo file_1 550 13 550 14.
  Definition loc_442 : location_info := LocationInfo file_1 550 17 550 25.
  Definition loc_443 : location_info := LocationInfo file_1 550 17 550 25.
  Definition loc_444 : location_info := LocationInfo file_1 550 6 550 7.
  Definition loc_445 : location_info := LocationInfo file_1 550 10 550 11.
  Definition loc_446 : location_info := LocationInfo file_1 547 1 547 7.
  Definition loc_447 : location_info := LocationInfo file_1 547 1 547 7.
  Definition loc_448 : location_info := LocationInfo file_1 547 8 547 9.
  Definition loc_449 : location_info := LocationInfo file_1 547 8 547 9.
  Definition loc_450 : location_info := LocationInfo file_1 547 11 547 12.
  Definition loc_451 : location_info := LocationInfo file_1 547 14 547 35.
  Definition loc_452 : location_info := LocationInfo file_1 547 14 547 24.
  Definition loc_453 : location_info := LocationInfo file_1 547 27 547 35.
  Definition loc_454 : location_info := LocationInfo file_1 547 27 547 35.
  Definition loc_455 : location_info := LocationInfo file_1 546 1 546 2.
  Definition loc_456 : location_info := LocationInfo file_1 546 5 546 27.
  Definition loc_457 : location_info := LocationInfo file_1 546 5 546 21.
  Definition loc_458 : location_info := LocationInfo file_1 546 5 546 21.
  Definition loc_459 : location_info := LocationInfo file_1 546 22 546 26.
  Definition loc_460 : location_info := LocationInfo file_1 546 22 546 26.
  Definition loc_461 : location_info := LocationInfo file_1 543 1 543 16.
  Definition loc_462 : location_info := LocationInfo file_1 543 1 543 5.
  Definition loc_463 : location_info := LocationInfo file_1 543 1 543 5.
  Definition loc_464 : location_info := LocationInfo file_1 543 19 543 42.
  Definition loc_465 : location_info := LocationInfo file_1 543 19 543 23.
  Definition loc_466 : location_info := LocationInfo file_1 543 19 543 23.
  Definition loc_467 : location_info := LocationInfo file_1 543 26 543 42.
  Definition loc_468 : location_info := LocationInfo file_1 543 27 543 35.
  Definition loc_469 : location_info := LocationInfo file_1 543 27 543 35.
  Definition loc_470 : location_info := LocationInfo file_1 543 39 543 41.
  Definition loc_471 : location_info := LocationInfo file_1 542 1 542 18.
  Definition loc_472 : location_info := LocationInfo file_1 542 1 542 5.
  Definition loc_473 : location_info := LocationInfo file_1 542 1 542 5.
  Definition loc_474 : location_info := LocationInfo file_1 542 21 542 25.
  Definition loc_475 : location_info := LocationInfo file_1 542 21 542 25.
  Definition loc_476 : location_info := LocationInfo file_1 540 1 541 38.
  Definition loc_477 : location_info := LocationInfo file_1 541 2 541 38.
  Definition loc_478 : location_info := LocationInfo file_1 540 1 541 38.
  Definition loc_479 : location_info := LocationInfo file_1 540 23 540 26.
  Definition loc_480 : location_info := LocationInfo file_1 540 23 540 24.
  Definition loc_481 : location_info := LocationInfo file_1 541 2 541 16.
  Definition loc_482 : location_info := LocationInfo file_1 541 2 541 16.
  Definition loc_483 : location_info := LocationInfo file_1 541 17 541 36.
  Definition loc_484 : location_info := LocationInfo file_1 541 18 541 36.
  Definition loc_485 : location_info := LocationInfo file_1 541 18 541 36.
  Definition loc_486 : location_info := LocationInfo file_1 541 18 541 33.
  Definition loc_487 : location_info := LocationInfo file_1 541 18 541 33.
  Definition loc_488 : location_info := LocationInfo file_1 541 18 541 22.
  Definition loc_489 : location_info := LocationInfo file_1 541 18 541 22.
  Definition loc_490 : location_info := LocationInfo file_1 541 34 541 35.
  Definition loc_491 : location_info := LocationInfo file_1 541 34 541 35.
  Definition loc_492 : location_info := LocationInfo file_1 540 13 540 21.
  Definition loc_493 : location_info := LocationInfo file_1 540 13 540 14.
  Definition loc_494 : location_info := LocationInfo file_1 540 13 540 14.
  Definition loc_495 : location_info := LocationInfo file_1 540 18 540 21.
  Definition loc_496 : location_info := LocationInfo file_1 540 6 540 7.
  Definition loc_497 : location_info := LocationInfo file_1 540 10 540 11.
  Definition loc_498 : location_info := LocationInfo file_1 539 1 539 8.
  Definition loc_499 : location_info := LocationInfo file_1 539 1 539 8.
  Definition loc_500 : location_info := LocationInfo file_1 539 9 539 20.
  Definition loc_501 : location_info := LocationInfo file_1 539 10 539 20.
  Definition loc_502 : location_info := LocationInfo file_1 539 10 539 14.
  Definition loc_503 : location_info := LocationInfo file_1 539 10 539 14.
  Definition loc_504 : location_info := LocationInfo file_1 537 2 537 13.
  Definition loc_505 : location_info := LocationInfo file_1 537 9 537 12.
  Definition loc_506 : location_info := LocationInfo file_1 537 10 537 12.
  Definition loc_508 : location_info := LocationInfo file_1 536 5 536 16.
  Definition loc_509 : location_info := LocationInfo file_1 536 5 536 9.
  Definition loc_510 : location_info := LocationInfo file_1 536 5 536 9.
  Definition loc_511 : location_info := LocationInfo file_1 536 12 536 16.
  Definition loc_514 : location_info := LocationInfo file_1 373 1 373 15.
  Definition loc_515 : location_info := LocationInfo file_1 373 15 373 2.
  Definition loc_516 : location_info := LocationInfo file_1 374 1 374 40.
  Definition loc_517 : location_info := LocationInfo file_1 376 1 376 25.
  Definition loc_518 : location_info := LocationInfo file_1 377 1 378 24.
  Definition loc_519 : location_info := LocationInfo file_1 380 1 380 31.
  Definition loc_520 : location_info := LocationInfo file_1 380 8 380 30.
  Definition loc_521 : location_info := LocationInfo file_1 380 8 380 24.
  Definition loc_522 : location_info := LocationInfo file_1 380 8 380 24.
  Definition loc_523 : location_info := LocationInfo file_1 380 25 380 29.
  Definition loc_524 : location_info := LocationInfo file_1 380 25 380 29.
  Definition loc_525 : location_info := LocationInfo file_1 378 2 378 24.
  Definition loc_526 : location_info := LocationInfo file_1 378 9 378 23.
  Definition loc_529 : location_info := LocationInfo file_1 377 5 377 29.
  Definition loc_530 : location_info := LocationInfo file_1 377 5 377 9.
  Definition loc_531 : location_info := LocationInfo file_1 377 5 377 9.
  Definition loc_532 : location_info := LocationInfo file_1 377 12 377 29.
  Definition loc_533 : location_info := LocationInfo file_1 377 12 377 29.
  Definition loc_534 : location_info := LocationInfo file_1 377 12 377 16.
  Definition loc_535 : location_info := LocationInfo file_1 377 12 377 16.
  Definition loc_536 : location_info := LocationInfo file_1 377 33 377 56.
  Definition loc_537 : location_info := LocationInfo file_1 377 33 377 37.
  Definition loc_538 : location_info := LocationInfo file_1 377 33 377 37.
  Definition loc_539 : location_info := LocationInfo file_1 377 41 377 56.
  Definition loc_540 : location_info := LocationInfo file_1 377 41 377 56.
  Definition loc_541 : location_info := LocationInfo file_1 377 41 377 45.
  Definition loc_542 : location_info := LocationInfo file_1 377 41 377 45.
  Definition loc_543 : location_info := LocationInfo file_1 376 1 376 5.
  Definition loc_544 : location_info := LocationInfo file_1 376 1 376 24.
  Definition loc_545 : location_info := LocationInfo file_1 376 1 376 5.
  Definition loc_546 : location_info := LocationInfo file_1 376 1 376 5.
  Definition loc_547 : location_info := LocationInfo file_1 376 9 376 24.
  Definition loc_548 : location_info := LocationInfo file_1 376 10 376 14.
  Definition loc_549 : location_info := LocationInfo file_1 376 18 376 23.
  Definition loc_550 : location_info := LocationInfo file_1 376 18 376 23.
  Definition loc_551 : location_info := LocationInfo file_1 374 20 374 39.
  Definition loc_552 : location_info := LocationInfo file_1 374 20 374 36.
  Definition loc_553 : location_info := LocationInfo file_1 374 20 374 36.
  Definition loc_554 : location_info := LocationInfo file_1 374 37 374 38.
  Definition loc_555 : location_info := LocationInfo file_1 374 37 374 38.
  Definition loc_558 : location_info := LocationInfo file_1 373 1 373 14.
  Definition loc_559 : location_info := LocationInfo file_1 373 2 373 14.
  Definition loc_560 : location_info := LocationInfo file_1 373 3 373 7.
  Definition loc_561 : location_info := LocationInfo file_1 373 3 373 7.
  Definition loc_564 : location_info := LocationInfo file_1 397 1 397 15.
  Definition loc_565 : location_info := LocationInfo file_1 397 15 397 2.
  Definition loc_566 : location_info := LocationInfo file_1 398 1 398 31.
  Definition loc_567 : location_info := LocationInfo file_1 401 1 401 31.
  Definition loc_568 : location_info := LocationInfo file_1 409 1 428 2.
  Definition loc_569 : location_info := LocationInfo file_1 429 1 429 15.
  Definition loc_570 : location_info := LocationInfo file_1 429 15 429 2.
  Definition loc_571 : location_info := LocationInfo file_1 431 1 431 18.
  Definition loc_572 : location_info := LocationInfo file_1 434 1 434 45.
  Definition loc_573 : location_info := LocationInfo file_1 434 1 434 9.
  Definition loc_574 : location_info := LocationInfo file_1 434 1 434 9.
  Definition loc_575 : location_info := LocationInfo file_1 434 10 434 18.
  Definition loc_576 : location_info := LocationInfo file_1 434 11 434 18.
  Definition loc_577 : location_info := LocationInfo file_1 434 11 434 12.
  Definition loc_578 : location_info := LocationInfo file_1 434 11 434 12.
  Definition loc_579 : location_info := LocationInfo file_1 434 20 434 43.
  Definition loc_580 : location_info := LocationInfo file_1 434 21 434 43.
  Definition loc_581 : location_info := LocationInfo file_1 434 21 434 43.
  Definition loc_582 : location_info := LocationInfo file_1 434 21 434 36.
  Definition loc_583 : location_info := LocationInfo file_1 434 21 434 36.
  Definition loc_584 : location_info := LocationInfo file_1 434 21 434 25.
  Definition loc_585 : location_info := LocationInfo file_1 434 21 434 25.
  Definition loc_586 : location_info := LocationInfo file_1 434 37 434 42.
  Definition loc_587 : location_info := LocationInfo file_1 434 37 434 42.
  Definition loc_588 : location_info := LocationInfo file_1 431 1 431 9.
  Definition loc_589 : location_info := LocationInfo file_1 431 1 431 2.
  Definition loc_590 : location_info := LocationInfo file_1 431 1 431 2.
  Definition loc_591 : location_info := LocationInfo file_1 431 12 431 17.
  Definition loc_592 : location_info := LocationInfo file_1 431 12 431 17.
  Definition loc_593 : location_info := LocationInfo file_1 429 1 429 14.
  Definition loc_594 : location_info := LocationInfo file_1 429 2 429 14.
  Definition loc_595 : location_info := LocationInfo file_1 429 3 429 7.
  Definition loc_596 : location_info := LocationInfo file_1 429 3 429 7.
  Definition loc_597 : location_info := LocationInfo file_1 409 30 428 2.
  Definition loc_598 : location_info := LocationInfo file_1 411 2 411 39.
  Definition loc_599 : location_info := LocationInfo file_1 412 2 412 16.
  Definition loc_600 : location_info := LocationInfo file_1 412 16 412 3.
  Definition loc_601 : location_info := LocationInfo file_1 415 2 416 9.
  Definition loc_602 : location_info := LocationInfo file_1 419 2 419 30.
  Definition loc_603 : location_info := LocationInfo file_1 420 2 420 36.
  Definition loc_604 : location_info := LocationInfo file_1 423 2 427 3.
  Definition loc_605 : location_info := LocationInfo file_1 409 1 428 2.
  Definition loc_606 : location_info := LocationInfo file_1 409 21 409 28.
  Definition loc_607 : location_info := LocationInfo file_1 409 21 409 26.
  Definition loc_608 : location_info := LocationInfo file_1 423 17 425 3.
  Definition loc_609 : location_info := LocationInfo file_1 424 3 424 9.
  Definition loc_610 : location_info := LocationInfo file_1 424 3 424 4.
  Definition loc_611 : location_info := LocationInfo file_1 424 7 424 8.
  Definition loc_612 : location_info := LocationInfo file_1 424 7 424 8.
  Definition loc_613 : location_info := LocationInfo file_1 425 9 427 3.
  Definition loc_614 : location_info := LocationInfo file_1 426 3 426 13.
  Definition loc_615 : location_info := LocationInfo file_1 426 3 426 4.
  Definition loc_616 : location_info := LocationInfo file_1 426 7 426 12.
  Definition loc_617 : location_info := LocationInfo file_1 426 7 426 12.
  Definition loc_618 : location_info := LocationInfo file_1 423 6 423 15.
  Definition loc_619 : location_info := LocationInfo file_1 423 6 423 7.
  Definition loc_620 : location_info := LocationInfo file_1 423 6 423 7.
  Definition loc_621 : location_info := LocationInfo file_1 423 10 423 15.
  Definition loc_622 : location_info := LocationInfo file_1 423 10 423 15.
  Definition loc_623 : location_info := LocationInfo file_1 420 2 420 14.
  Definition loc_624 : location_info := LocationInfo file_1 420 2 420 7.
  Definition loc_625 : location_info := LocationInfo file_1 420 2 420 7.
  Definition loc_626 : location_info := LocationInfo file_1 420 17 420 35.
  Definition loc_627 : location_info := LocationInfo file_1 419 2 419 15.
  Definition loc_628 : location_info := LocationInfo file_1 419 2 419 15.
  Definition loc_629 : location_info := LocationInfo file_1 419 16 419 28.
  Definition loc_630 : location_info := LocationInfo file_1 419 17 419 28.
  Definition loc_631 : location_info := LocationInfo file_1 419 17 419 22.
  Definition loc_632 : location_info := LocationInfo file_1 419 17 419 22.
  Definition loc_633 : location_info := LocationInfo file_1 416 3 416 9.
  Definition loc_637 : location_info := LocationInfo file_1 415 6 415 29.
  Definition loc_638 : location_info := LocationInfo file_1 415 6 415 11.
  Definition loc_639 : location_info := LocationInfo file_1 415 6 415 11.
  Definition loc_640 : location_info := LocationInfo file_1 415 15 415 29.
  Definition loc_641 : location_info := LocationInfo file_1 415 33 415 57.
  Definition loc_642 : location_info := LocationInfo file_1 415 33 415 43.
  Definition loc_643 : location_info := LocationInfo file_1 415 33 415 43.
  Definition loc_644 : location_info := LocationInfo file_1 415 44 415 56.
  Definition loc_645 : location_info := LocationInfo file_1 415 45 415 56.
  Definition loc_646 : location_info := LocationInfo file_1 415 45 415 50.
  Definition loc_647 : location_info := LocationInfo file_1 415 45 415 50.
  Definition loc_648 : location_info := LocationInfo file_1 415 61 415 82.
  Definition loc_649 : location_info := LocationInfo file_1 415 61 415 73.
  Definition loc_650 : location_info := LocationInfo file_1 415 61 415 73.
  Definition loc_651 : location_info := LocationInfo file_1 415 61 415 66.
  Definition loc_652 : location_info := LocationInfo file_1 415 61 415 66.
  Definition loc_653 : location_info := LocationInfo file_1 415 77 415 82.
  Definition loc_654 : location_info := LocationInfo file_1 415 77 415 82.
  Definition loc_655 : location_info := LocationInfo file_1 412 2 412 15.
  Definition loc_656 : location_info := LocationInfo file_1 412 3 412 15.
  Definition loc_657 : location_info := LocationInfo file_1 412 4 412 8.
  Definition loc_658 : location_info := LocationInfo file_1 412 4 412 8.
  Definition loc_659 : location_info := LocationInfo file_1 411 2 411 7.
  Definition loc_660 : location_info := LocationInfo file_1 411 10 411 38.
  Definition loc_661 : location_info := LocationInfo file_1 411 10 411 22.
  Definition loc_662 : location_info := LocationInfo file_1 411 10 411 22.
  Definition loc_663 : location_info := LocationInfo file_1 411 23 411 27.
  Definition loc_664 : location_info := LocationInfo file_1 411 23 411 27.
  Definition loc_665 : location_info := LocationInfo file_1 411 29 411 30.
  Definition loc_666 : location_info := LocationInfo file_1 411 29 411 30.
  Definition loc_667 : location_info := LocationInfo file_1 411 32 411 37.
  Definition loc_668 : location_info := LocationInfo file_1 411 32 411 37.
  Definition loc_669 : location_info := LocationInfo file_1 409 8 409 19.
  Definition loc_670 : location_info := LocationInfo file_1 409 8 409 13.
  Definition loc_671 : location_info := LocationInfo file_1 409 8 409 13.
  Definition loc_672 : location_info := LocationInfo file_1 409 16 409 19.
  Definition loc_673 : location_info := LocationInfo file_1 401 1 401 9.
  Definition loc_674 : location_info := LocationInfo file_1 401 1 401 2.
  Definition loc_675 : location_info := LocationInfo file_1 401 1 401 2.
  Definition loc_676 : location_info := LocationInfo file_1 401 12 401 30.
  Definition loc_677 : location_info := LocationInfo file_1 398 22 398 30.
  Definition loc_678 : location_info := LocationInfo file_1 398 22 398 30.
  Definition loc_679 : location_info := LocationInfo file_1 398 22 398 23.
  Definition loc_680 : location_info := LocationInfo file_1 398 22 398 23.
  Definition loc_683 : location_info := LocationInfo file_1 397 1 397 14.
  Definition loc_684 : location_info := LocationInfo file_1 397 2 397 14.
  Definition loc_685 : location_info := LocationInfo file_1 397 3 397 7.
  Definition loc_686 : location_info := LocationInfo file_1 397 3 397 7.
  Definition loc_689 : location_info := LocationInfo file_1 468 1 469 24.
  Definition loc_690 : location_info := LocationInfo file_1 471 1 471 25.
  Definition loc_691 : location_info := LocationInfo file_1 474 1 479 2.
  Definition loc_692 : location_info := LocationInfo file_1 481 1 481 17.
  Definition loc_693 : location_info := LocationInfo file_1 483 1 483 10.
  Definition loc_694 : location_info := LocationInfo file_1 483 8 483 9.
  Definition loc_695 : location_info := LocationInfo file_1 483 8 483 9.
  Definition loc_696 : location_info := LocationInfo file_1 481 1 481 12.
  Definition loc_697 : location_info := LocationInfo file_1 481 1 481 2.
  Definition loc_698 : location_info := LocationInfo file_1 481 1 481 2.
  Definition loc_699 : location_info := LocationInfo file_1 481 15 481 16.
  Definition loc_700 : location_info := LocationInfo file_1 474 1 479 2.
  Definition loc_701 : location_info := LocationInfo file_1 474 26 479 2.
  Definition loc_702 : location_info := LocationInfo file_1 475 2 475 13.
  Definition loc_703 : location_info := LocationInfo file_1 476 2 476 42.
  Definition loc_704 : location_info := LocationInfo file_1 477 2 477 26.
  Definition loc_705 : location_info := LocationInfo file_1 478 2 478 62.
  Definition loc_706 : location_info := LocationInfo file_1 474 1 479 2.
  Definition loc_707 : location_info := LocationInfo file_1 474 1 479 2.
  Definition loc_708 : location_info := LocationInfo file_1 478 2 478 15.
  Definition loc_709 : location_info := LocationInfo file_1 478 2 478 15.
  Definition loc_710 : location_info := LocationInfo file_1 478 16 478 28.
  Definition loc_711 : location_info := LocationInfo file_1 478 17 478 28.
  Definition loc_712 : location_info := LocationInfo file_1 478 17 478 22.
  Definition loc_713 : location_info := LocationInfo file_1 478 17 478 22.
  Definition loc_714 : location_info := LocationInfo file_1 478 30 478 60.
  Definition loc_715 : location_info := LocationInfo file_1 478 31 478 60.
  Definition loc_716 : location_info := LocationInfo file_1 478 31 478 60.
  Definition loc_717 : location_info := LocationInfo file_1 478 31 478 46.
  Definition loc_718 : location_info := LocationInfo file_1 478 31 478 46.
  Definition loc_719 : location_info := LocationInfo file_1 478 31 478 35.
  Definition loc_720 : location_info := LocationInfo file_1 478 31 478 35.
  Definition loc_721 : location_info := LocationInfo file_1 478 47 478 59.
  Definition loc_722 : location_info := LocationInfo file_1 478 47 478 59.
  Definition loc_723 : location_info := LocationInfo file_1 478 47 478 52.
  Definition loc_724 : location_info := LocationInfo file_1 478 47 478 52.
  Definition loc_725 : location_info := LocationInfo file_1 477 2 477 14.
  Definition loc_726 : location_info := LocationInfo file_1 477 2 477 7.
  Definition loc_727 : location_info := LocationInfo file_1 477 2 477 7.
  Definition loc_728 : location_info := LocationInfo file_1 477 17 477 25.
  Definition loc_729 : location_info := LocationInfo file_1 477 17 477 25.
  Definition loc_730 : location_info := LocationInfo file_1 477 17 477 18.
  Definition loc_731 : location_info := LocationInfo file_1 477 17 477 18.
  Definition loc_732 : location_info := LocationInfo file_1 476 2 476 7.
  Definition loc_733 : location_info := LocationInfo file_1 476 10 476 41.
  Definition loc_734 : location_info := LocationInfo file_1 476 10 476 22.
  Definition loc_735 : location_info := LocationInfo file_1 476 10 476 22.
  Definition loc_736 : location_info := LocationInfo file_1 476 23 476 27.
  Definition loc_737 : location_info := LocationInfo file_1 476 23 476 27.
  Definition loc_738 : location_info := LocationInfo file_1 476 29 476 30.
  Definition loc_739 : location_info := LocationInfo file_1 476 29 476 30.
  Definition loc_740 : location_info := LocationInfo file_1 476 32 476 40.
  Definition loc_741 : location_info := LocationInfo file_1 476 32 476 40.
  Definition loc_742 : location_info := LocationInfo file_1 476 32 476 33.
  Definition loc_743 : location_info := LocationInfo file_1 476 32 476 33.
  Definition loc_744 : location_info := LocationInfo file_1 475 2 475 10.
  Definition loc_745 : location_info := LocationInfo file_1 475 2 475 3.
  Definition loc_746 : location_info := LocationInfo file_1 475 2 475 3.
  Definition loc_747 : location_info := LocationInfo file_1 474 8 474 24.
  Definition loc_748 : location_info := LocationInfo file_1 474 8 474 16.
  Definition loc_749 : location_info := LocationInfo file_1 474 8 474 16.
  Definition loc_750 : location_info := LocationInfo file_1 474 8 474 9.
  Definition loc_751 : location_info := LocationInfo file_1 474 8 474 9.
  Definition loc_752 : location_info := LocationInfo file_1 474 19 474 24.
  Definition loc_753 : location_info := LocationInfo file_1 474 19 474 24.
  Definition loc_754 : location_info := LocationInfo file_1 471 1 471 14.
  Definition loc_755 : location_info := LocationInfo file_1 471 1 471 14.
  Definition loc_756 : location_info := LocationInfo file_1 471 15 471 23.
  Definition loc_757 : location_info := LocationInfo file_1 471 16 471 23.
  Definition loc_758 : location_info := LocationInfo file_1 471 16 471 17.
  Definition loc_759 : location_info := LocationInfo file_1 471 16 471 17.
  Definition loc_760 : location_info := LocationInfo file_1 469 2 469 24.
  Definition loc_761 : location_info := LocationInfo file_1 469 9 469 23.
  Definition loc_764 : location_info := LocationInfo file_1 468 5 468 35.
  Definition loc_765 : location_info := LocationInfo file_1 468 5 468 13.
  Definition loc_766 : location_info := LocationInfo file_1 468 5 468 13.
  Definition loc_767 : location_info := LocationInfo file_1 468 5 468 6.
  Definition loc_768 : location_info := LocationInfo file_1 468 5 468 6.
  Definition loc_769 : location_info := LocationInfo file_1 468 17 468 35.
  Definition loc_770 : location_info := LocationInfo file_1 468 39 468 55.
  Definition loc_771 : location_info := LocationInfo file_1 468 39 468 47.
  Definition loc_772 : location_info := LocationInfo file_1 468 39 468 47.
  Definition loc_773 : location_info := LocationInfo file_1 468 39 468 40.
  Definition loc_774 : location_info := LocationInfo file_1 468 39 468 40.
  Definition loc_775 : location_info := LocationInfo file_1 468 50 468 55.
  Definition loc_776 : location_info := LocationInfo file_1 468 50 468 55.
  Definition loc_779 : location_info := LocationInfo file_1 490 6 490 11.
  Definition loc_780 : location_info := LocationInfo file_1 490 1 491 112.
  Definition loc_781 : location_info := LocationInfo file_1 490 1 491 112.
  Definition loc_782 : location_info := LocationInfo file_1 491 2 491 112.
  Definition loc_783 : location_info := LocationInfo file_1 490 1 491 112.
  Definition loc_784 : location_info := LocationInfo file_1 490 34 490 37.
  Definition loc_785 : location_info := LocationInfo file_1 490 34 490 35.
  Definition loc_786 : location_info := LocationInfo file_1 491 2 491 12.
  Definition loc_787 : location_info := LocationInfo file_1 491 2 491 12.
  Definition loc_788 : location_info := LocationInfo file_1 491 13 491 110.
  Definition loc_789 : location_info := LocationInfo file_1 491 13 491 98.
  Definition loc_790 : location_info := LocationInfo file_1 491 30 491 98.
  Definition loc_791 : location_info := LocationInfo file_1 491 39 491 97.
  Definition loc_792 : location_info := LocationInfo file_1 491 40 491 74.
  Definition loc_793 : location_info := LocationInfo file_1 491 53 491 74.
  Definition loc_794 : location_info := LocationInfo file_1 491 54 491 70.
  Definition loc_795 : location_info := LocationInfo file_1 491 54 491 70.
  Definition loc_796 : location_info := LocationInfo file_1 491 71 491 72.
  Definition loc_797 : location_info := LocationInfo file_1 491 71 491 72.
  Definition loc_798 : location_info := LocationInfo file_1 491 77 491 96.
  Definition loc_799 : location_info := LocationInfo file_1 491 77 491 96.
  Definition loc_800 : location_info := LocationInfo file_1 491 101 491 110.
  Definition loc_801 : location_info := LocationInfo file_1 491 102 491 103.
  Definition loc_802 : location_info := LocationInfo file_1 491 102 491 103.
  Definition loc_803 : location_info := LocationInfo file_1 491 107 491 109.
  Definition loc_804 : location_info := LocationInfo file_1 490 13 490 32.
  Definition loc_805 : location_info := LocationInfo file_1 490 13 490 14.
  Definition loc_806 : location_info := LocationInfo file_1 490 13 490 14.
  Definition loc_807 : location_info := LocationInfo file_1 490 17 490 32.
  Definition loc_808 : location_info := LocationInfo file_1 490 18 490 19.
  Definition loc_809 : location_info := LocationInfo file_1 490 23 490 31.
  Definition loc_810 : location_info := LocationInfo file_1 490 23 490 31.
  Definition loc_811 : location_info := LocationInfo file_1 490 23 490 24.
  Definition loc_812 : location_info := LocationInfo file_1 490 23 490 24.
  Definition loc_813 : location_info := LocationInfo file_1 490 6 490 7.
  Definition loc_814 : location_info := LocationInfo file_1 490 10 490 11.
  Definition loc_817 : location_info := LocationInfo file_1 499 1 499 24.
  Definition loc_818 : location_info := LocationInfo file_1 503 1 504 6.
  Definition loc_819 : location_info := LocationInfo file_1 505 1 506 24.
  Definition loc_820 : location_info := LocationInfo file_1 509 1 509 99.
  Definition loc_821 : location_info := LocationInfo file_1 510 1 510 40.
  Definition loc_822 : location_info := LocationInfo file_1 512 1 513 20.
  Definition loc_823 : location_info := LocationInfo file_1 515 1 515 10.
  Definition loc_824 : location_info := LocationInfo file_1 515 8 515 9.
  Definition loc_825 : location_info := LocationInfo file_1 515 8 515 9.
  Definition loc_826 : location_info := LocationInfo file_1 513 2 513 20.
  Definition loc_827 : location_info := LocationInfo file_1 513 2 513 16.
  Definition loc_828 : location_info := LocationInfo file_1 513 2 513 16.
  Definition loc_829 : location_info := LocationInfo file_1 513 17 513 18.
  Definition loc_830 : location_info := LocationInfo file_1 513 17 513 18.
  Definition loc_832 : location_info := LocationInfo file_1 512 5 512 13.
  Definition loc_833 : location_info := LocationInfo file_1 512 5 512 9.
  Definition loc_834 : location_info := LocationInfo file_1 512 5 512 9.
  Definition loc_835 : location_info := LocationInfo file_1 512 12 512 13.
  Definition loc_836 : location_info := LocationInfo file_1 510 1 510 2.
  Definition loc_837 : location_info := LocationInfo file_1 510 5 510 39.
  Definition loc_838 : location_info := LocationInfo file_1 510 5 510 23.
  Definition loc_839 : location_info := LocationInfo file_1 510 5 510 23.
  Definition loc_840 : location_info := LocationInfo file_1 510 24 510 28.
  Definition loc_841 : location_info := LocationInfo file_1 510 24 510 28.
  Definition loc_842 : location_info := LocationInfo file_1 510 30 510 31.
  Definition loc_843 : location_info := LocationInfo file_1 510 30 510 31.
  Definition loc_844 : location_info := LocationInfo file_1 510 33 510 38.
  Definition loc_845 : location_info := LocationInfo file_1 510 33 510 38.
  Definition loc_846 : location_info := LocationInfo file_1 509 1 509 2.
  Definition loc_847 : location_info := LocationInfo file_1 509 5 509 98.
  Definition loc_848 : location_info := LocationInfo file_1 509 24 509 98.
  Definition loc_849 : location_info := LocationInfo file_1 509 26 509 63.
  Definition loc_850 : location_info := LocationInfo file_1 509 34 509 63.
  Definition loc_851 : location_info := LocationInfo file_1 509 34 509 63.
  Definition loc_852 : location_info := LocationInfo file_1 509 35 509 56.
  Definition loc_853 : location_info := LocationInfo file_1 509 37 509 55.
  Definition loc_854 : location_info := LocationInfo file_1 509 37 509 55.
  Definition loc_855 : location_info := LocationInfo file_1 509 37 509 52.
  Definition loc_856 : location_info := LocationInfo file_1 509 37 509 52.
  Definition loc_857 : location_info := LocationInfo file_1 509 37 509 41.
  Definition loc_858 : location_info := LocationInfo file_1 509 37 509 41.
  Definition loc_859 : location_info := LocationInfo file_1 509 53 509 54.
  Definition loc_860 : location_info := LocationInfo file_1 509 53 509 54.
  Definition loc_861 : location_info := LocationInfo file_1 509 66 509 96.
  Definition loc_862 : location_info := LocationInfo file_1 506 2 506 24.
  Definition loc_863 : location_info := LocationInfo file_1 506 9 506 23.
  Definition loc_865 : location_info := LocationInfo file_1 505 5 505 12.
  Definition loc_866 : location_info := LocationInfo file_1 505 5 505 6.
  Definition loc_867 : location_info := LocationInfo file_1 505 5 505 6.
  Definition loc_868 : location_info := LocationInfo file_1 505 9 505 12.
  Definition loc_869 : location_info := LocationInfo file_1 503 1 504 6.
  Definition loc_870 : location_info := LocationInfo file_1 504 2 504 6.
  Definition loc_871 : location_info := LocationInfo file_1 503 1 504 6.
  Definition loc_872 : location_info := LocationInfo file_1 503 1 504 6.
  Definition loc_873 : location_info := LocationInfo file_1 504 2 504 3.
  Definition loc_875 : location_info := LocationInfo file_1 503 8 503 16.
  Definition loc_876 : location_info := LocationInfo file_1 503 8 503 9.
  Definition loc_877 : location_info := LocationInfo file_1 503 8 503 9.
  Definition loc_878 : location_info := LocationInfo file_1 503 13 503 16.
  Definition loc_879 : location_info := LocationInfo file_1 503 20 503 51.
  Definition loc_880 : location_info := LocationInfo file_1 503 20 503 30.
  Definition loc_881 : location_info := LocationInfo file_1 503 20 503 30.
  Definition loc_882 : location_info := LocationInfo file_1 503 31 503 50.
  Definition loc_883 : location_info := LocationInfo file_1 503 32 503 50.
  Definition loc_884 : location_info := LocationInfo file_1 503 32 503 50.
  Definition loc_885 : location_info := LocationInfo file_1 503 32 503 47.
  Definition loc_886 : location_info := LocationInfo file_1 503 32 503 47.
  Definition loc_887 : location_info := LocationInfo file_1 503 32 503 36.
  Definition loc_888 : location_info := LocationInfo file_1 503 32 503 36.
  Definition loc_889 : location_info := LocationInfo file_1 503 48 503 49.
  Definition loc_890 : location_info := LocationInfo file_1 503 48 503 49.
  Definition loc_891 : location_info := LocationInfo file_1 499 18 499 23.
  Definition loc_892 : location_info := LocationInfo file_1 499 18 499 23.
Michael Sammler's avatar
Michael Sammler committed
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873

  (* Definition of struct [atomic_flag]. *)
  Program Definition struct_atomic_flag := {|
    sl_members := [
      (Some "_Value", it_layout bool_it)
    ];
  |}.
  Solve Obligations with solve_struct_obligations.

  (* Definition of struct [spinlock]. *)
  Program Definition struct_spinlock := {|
    sl_members := [
      (Some "lock", it_layout bool_it)
    ];
  |}.
  Solve Obligations with solve_struct_obligations.

  (* Definition of struct [list_head]. *)
  Program Definition struct_list_head := {|
    sl_members := [
      (Some "next", void*);
      (Some "prev", void*)
    ];
  |}.
  Solve Obligations with solve_struct_obligations.

  (* Definition of struct [hyp_memblock_region]. *)
  Program Definition struct_hyp_memblock_region := {|
    sl_members := [
      (Some "start", it_layout u64);
      (Some "end", it_layout u64)
    ];
  |}.
  Solve Obligations with solve_struct_obligations.

  (* Definition of struct [hyp_page]. *)
  Program Definition struct_hyp_page := {|
    sl_members := [
      (Some "refcount", it_layout u32);
      (Some "order", it_layout u32);
      (Some "pool", void*);
      (Some "node", layout_of struct_list_head)
    ];
  |}.
  Solve Obligations with solve_struct_obligations.

  (* Definition of struct [hyp_pool]. *)
  Program Definition struct_hyp_pool := {|
    sl_members := [
      (Some "lock", layout_of struct_spinlock);
      (None, Layout 7%nat 0%nat);
      (Some "free_area", mk_array_layout (layout_of struct_list_head) 12);
      (Some "range_start", it_layout u64);
      (Some "range_end", it_layout u64)
    ];
  |}.
  Solve Obligations with solve_struct_obligations.

874
875
876
877
878
879
880
881
882
883
884
885
  (* 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
886
        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"))))))
887
888
889
890
      ]> $
    )%E
  |}.

Michael Sammler's avatar
Michael Sammler committed
891
892
893
894
895
896
897
898
899
  (* Definition of function [hyp_panic]. *)
  Definition impl_hyp_panic : function := {|
    f_args := [
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
900
901
        locinfo: loc_11 ;
        assert: (LocInfoE loc_12 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_12 (i2v 0 i32)))) ;
Michael Sammler's avatar
Michael Sammler committed
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
        Return (VOID)
      ]> $
    )%E
  |}.

  (* Definition of function [__list_add_valid]. *)
  Definition impl___list_add_valid : function := {|
    f_args := [
      ("new", void*);
      ("prev", void*);
      ("next", void*)
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
919
920
        locinfo: loc_15 ;
        Return (LocInfoE loc_16 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_16 (i2v 1 i32))))
Michael Sammler's avatar
Michael Sammler committed
921
922
923
924
925
926
927
928
929
930
931
932
933
934
      ]> $
    )%E
  |}.

  (* Definition of function [__list_del_entry_valid]. *)
  Definition impl___list_del_entry_valid : function := {|
    f_args := [
      ("entry", void*)
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
935
936
        locinfo: loc_19 ;
        Return (LocInfoE loc_20 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_20 (i2v 1 i32))))
Michael Sammler's avatar
Michael Sammler committed
937
938
939
940
941
942
943
944
945
946
947
948
949
950
      ]> $
    )%E
  |}.

  (* Definition of function [INIT_LIST_HEAD]. *)
  Definition impl_INIT_LIST_HEAD : function := {|
    f_args := [
      ("list", void*)
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
951
        locinfo: loc_23 ;
Michael Sammler's avatar
Michael Sammler committed
952
953
        LocInfoE loc_30 ((LocInfoE loc_31 (!{PtrOp} (LocInfoE loc_32 ("list")))) at{struct_list_head} "next") <-{ PtrOp }
          LocInfoE loc_33 (use{PtrOp} (LocInfoE loc_34 ("list"))) ;
954
        locinfo: loc_24 ;
Michael Sammler's avatar
Michael Sammler committed
955
956
        LocInfoE loc_25 ((LocInfoE loc_26 (!{PtrOp} (LocInfoE loc_27 ("list")))) at{struct_list_head} "prev") <-{ PtrOp }
          LocInfoE loc_28 (use{PtrOp} (LocInfoE loc_29 ("list"))) ;
Michael Sammler's avatar
Michael Sammler committed
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
        Return (VOID)
      ]> $
    )%E
  |}.

  (* Definition of function [__list_add]. *)
  Definition impl___list_add (global___list_add_valid : loc): function := {|
    f_args := [
      ("new", void*);
      ("prev", void*);
      ("next", void*)
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
974
        locinfo: loc_65 ;
Michael Sammler's avatar
Michael Sammler committed
975
976
977
        if: LocInfoE loc_65 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_65 ((i2v 0 i32) ={IntOp i32, IntOp i32} (LocInfoE loc_67 (UnOp (CastOp $ IntOp i32) (IntOp bool_it) (LocInfoE loc_67 (Call (LocInfoE loc_69 (global___list_add_valid)) [@{expr} LocInfoE loc_70 (use{PtrOp} (LocInfoE loc_71 ("new"))) ;
            LocInfoE loc_72 (use{PtrOp} (LocInfoE loc_73 ("prev"))) ;
            LocInfoE loc_74 (use{PtrOp} (LocInfoE loc_75 ("next"))) ])))))))
Michael Sammler's avatar
Michael Sammler committed
978
        then
979
        locinfo: loc_62 ;
Michael Sammler's avatar
Michael Sammler committed
980
981
          Goto "#2"
        else
982
        locinfo: loc_38 ;
Michael Sammler's avatar
Michael Sammler committed
983
984
985
          Goto "#3"
      ]> $
      <[ "#1" :=
986
        locinfo: loc_38 ;
Michael Sammler's avatar
Michael Sammler committed
987
988
        LocInfoE loc_57 ((LocInfoE loc_58 (!{PtrOp} (LocInfoE loc_59 ("next")))) at{struct_list_head} "prev") <-{ PtrOp }
          LocInfoE loc_60 (use{PtrOp} (LocInfoE loc_61 ("new"))) ;
989
        locinfo: loc_39 ;
Michael Sammler's avatar
Michael Sammler committed
990
991
        LocInfoE loc_52 ((LocInfoE loc_53 (!{PtrOp} (LocInfoE loc_54 ("new")))) at{struct_list_head} "next") <-{ PtrOp }
          LocInfoE loc_55 (use{PtrOp} (LocInfoE loc_56 ("next"))) ;
992
        locinfo: loc_40 ;
Michael Sammler's avatar
Michael Sammler committed
993
994
        LocInfoE loc_47 ((LocInfoE loc_48 (!{PtrOp} (LocInfoE loc_49 ("new")))) at{struct_list_head} "prev") <-{ PtrOp }
          LocInfoE loc_50 (use{PtrOp} (LocInfoE loc_51 ("prev"))) ;
995
        locinfo: loc_41 ;
Michael Sammler's avatar
Michael Sammler committed
996
997
        LocInfoE loc_42 ((LocInfoE loc_43 (!{PtrOp} (LocInfoE loc_44 ("prev")))) at{struct_list_head} "next") <-{ PtrOp }
          LocInfoE loc_45 (use{PtrOp} (LocInfoE loc_46 ("new"))) ;
Michael Sammler's avatar
Michael Sammler committed
998
999
1000
        Return (VOID)
      ]> $
      <[ "#2" :=