source: extracted/csem.ml @ 2717

Last change on this file since 2717 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 50.5 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open Hide
12
13open ByteValues
14
15open Division
16
17open Z
18
19open BitVectorZ
20
21open Pointers
22
23open GenMem
24
25open FrontEndMem
26
27open Proper
28
29open PositiveMap
30
31open Deqsets
32
33open Extralib
34
35open Lists
36
37open Identifiers
38
39open Exp
40
41open Arithmetic
42
43open Vector
44
45open Div_and_mod
46
47open Util
48
49open FoldStuff
50
51open BitVector
52
53open Extranat
54
55open Integers
56
57open AST
58
59open ErrorMessages
60
61open Option
62
63open Setoids
64
65open Monad
66
67open Jmeq
68
69open Russell
70
71open Positive
72
73open PreIdentifiers
74
75open Bool
76
77open Relations
78
79open Nat
80
81open List
82
83open Hints_declaration
84
85open Core_notation
86
87open Pts
88
89open Logic
90
91open Types
92
93open Errors
94
95open Globalenvs
96
97open BitVectorTrie
98
99open CostLabel
100
101open Csyntax
102
103open Events
104
105open Smallstep
106
107open TypeComparison
108
109open ClassifyOp
110
111(** val sem_neg :
112    Values.val0 -> Csyntax.type0 -> Values.val0 Types.option **)
113let rec sem_neg v = function
114| Csyntax.Tvoid -> Types.None
115| Csyntax.Tint (sz, x) ->
116  (match v with
117   | Values.Vundef -> Types.None
118   | Values.Vint (sz', n) ->
119     (match AST.eq_intsize sz sz' with
120      | Bool.True ->
121        Types.Some (Values.Vint (sz',
122          (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz') n)))
123      | Bool.False -> Types.None)
124   | Values.Vnull -> Types.None
125   | Values.Vptr x0 -> Types.None)
126| Csyntax.Tpointer x -> Types.None
127| Csyntax.Tarray (x, x0) -> Types.None
128| Csyntax.Tfunction (x, x0) -> Types.None
129| Csyntax.Tstruct (x, x0) -> Types.None
130| Csyntax.Tunion (x, x0) -> Types.None
131| Csyntax.Tcomp_ptr x -> Types.None
132
133(** val sem_notint : Values.val0 -> Values.val0 Types.option **)
134let rec sem_notint = function
135| Values.Vundef -> Types.None
136| Values.Vint (sz, n) ->
137  Types.Some (Values.Vint (sz,
138    (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz) n
139      (Values.mone0 sz))))
140| Values.Vnull -> Types.None
141| Values.Vptr x -> Types.None
142
143(** val sem_notbool :
144    Values.val0 -> Csyntax.type0 -> Values.val0 Types.option **)
145let rec sem_notbool v = function
146| Csyntax.Tvoid -> Types.None
147| Csyntax.Tint (sz, x) ->
148  (match v with
149   | Values.Vundef -> Types.None
150   | Values.Vint (sz', n) ->
151     (match AST.eq_intsize sz sz' with
152      | Bool.True ->
153        Types.Some
154          (Values.of_bool
155            (BitVector.eq_bv (AST.bitsize_of_intsize sz') n
156              (BitVector.zero (AST.bitsize_of_intsize sz'))))
157      | Bool.False -> Types.None)
158   | Values.Vnull -> Types.None
159   | Values.Vptr x0 -> Types.None)
160| Csyntax.Tpointer x ->
161  (match v with
162   | Values.Vundef -> Types.None
163   | Values.Vint (x0, x1) -> Types.None
164   | Values.Vnull -> Types.Some Values.vtrue
165   | Values.Vptr x0 -> Types.Some Values.vfalse)
166| Csyntax.Tarray (x, x0) -> Types.None
167| Csyntax.Tfunction (x, x0) -> Types.None
168| Csyntax.Tstruct (x, x0) -> Types.None
169| Csyntax.Tunion (x, x0) -> Types.None
170| Csyntax.Tcomp_ptr x -> Types.None
171
172(** val sem_add :
173    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
174    Values.val0 Types.option **)
175let rec sem_add v1 t1 v2 t2 =
176  match ClassifyOp.classify_add t1 t2 with
177  | ClassifyOp.Add_case_ii (x, x0) ->
178    (match v1 with
179     | Values.Vundef -> Types.None
180     | Values.Vint (sz1, n1) ->
181       (match v2 with
182        | Values.Vundef -> Types.None
183        | Values.Vint (sz2, n2) ->
184          AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
185            (sz2,
186            (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))))
187            Types.None
188        | Values.Vnull -> Types.None
189        | Values.Vptr x1 -> Types.None)
190     | Values.Vnull -> Types.None
191     | Values.Vptr x1 -> Types.None)
192  | ClassifyOp.Add_case_pi (x, ty, x0, sg) ->
193    (match v1 with
194     | Values.Vundef -> Types.None
195     | Values.Vint (x1, x2) -> Types.None
196     | Values.Vnull ->
197       (match v2 with
198        | Values.Vundef -> Types.None
199        | Values.Vint (sz2, n2) ->
200          (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
201                   (BitVector.zero (AST.bitsize_of_intsize sz2)) with
202           | Bool.True -> Types.Some Values.Vnull
203           | Bool.False -> Types.None)
204        | Values.Vnull -> Types.None
205        | Values.Vptr x1 -> Types.None)
206     | Values.Vptr ptr1 ->
207       (match v2 with
208        | Values.Vundef -> Types.None
209        | Values.Vint (sz2, n2) ->
210          Types.Some (Values.Vptr
211            (Pointers.shift_pointer_n (AST.bitsize_of_intsize sz2) ptr1
212              (Csyntax.sizeof ty) sg n2))
213        | Values.Vnull -> Types.None
214        | Values.Vptr x1 -> Types.None))
215  | ClassifyOp.Add_case_ip (x, x0, sg, ty) ->
216    (match v1 with
217     | Values.Vundef -> Types.None
218     | Values.Vint (sz1, n1) ->
219       (match v2 with
220        | Values.Vundef -> Types.None
221        | Values.Vint (x1, x2) -> Types.None
222        | Values.Vnull ->
223          (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
224                   (BitVector.zero (AST.bitsize_of_intsize sz1)) with
225           | Bool.True -> Types.Some Values.Vnull
226           | Bool.False -> Types.None)
227        | Values.Vptr ptr2 ->
228          Types.Some (Values.Vptr
229            (Pointers.shift_pointer_n (AST.bitsize_of_intsize sz1) ptr2
230              (Csyntax.sizeof ty) sg n1)))
231     | Values.Vnull -> Types.None
232     | Values.Vptr x1 -> Types.None)
233  | ClassifyOp.Add_default (x, x0) -> Types.None
234
235(** val sem_sub :
236    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
237    Csyntax.type0 -> Values.val0 Types.option **)
238let rec sem_sub v1 t1 v2 t2 target =
239  match ClassifyOp.classify_sub t1 t2 with
240  | ClassifyOp.Sub_case_ii (x, x0) ->
241    (match v1 with
242     | Values.Vundef -> Types.None
243     | Values.Vint (sz1, n1) ->
244       (match v2 with
245        | Values.Vundef -> Types.None
246        | Values.Vint (sz2, n2) ->
247          AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
248            (sz2,
249            (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2))))
250            Types.None
251        | Values.Vnull -> Types.None
252        | Values.Vptr x1 -> Types.None)
253     | Values.Vnull -> Types.None
254     | Values.Vptr x1 -> Types.None)
255  | ClassifyOp.Sub_case_pi (x, ty, x0, sg) ->
256    (match v1 with
257     | Values.Vundef -> Types.None
258     | Values.Vint (x1, x2) -> Types.None
259     | Values.Vnull ->
260       (match v2 with
261        | Values.Vundef -> Types.None
262        | Values.Vint (sz2, n2) ->
263          (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
264                   (BitVector.zero (AST.bitsize_of_intsize sz2)) with
265           | Bool.True -> Types.Some Values.Vnull
266           | Bool.False -> Types.None)
267        | Values.Vnull -> Types.None
268        | Values.Vptr x1 -> Types.None)
269     | Values.Vptr ptr1 ->
270       (match v2 with
271        | Values.Vundef -> Types.None
272        | Values.Vint (sz2, n2) ->
273          Types.Some (Values.Vptr
274            (Pointers.neg_shift_pointer_n (AST.bitsize_of_intsize sz2) ptr1
275              (Csyntax.sizeof ty) sg n2))
276        | Values.Vnull -> Types.None
277        | Values.Vptr x1 -> Types.None))
278  | ClassifyOp.Sub_case_pp (x, x0, ty, x1) ->
279    (match v1 with
280     | Values.Vundef -> Types.None
281     | Values.Vint (x2, x3) -> Types.None
282     | Values.Vnull ->
283       (match v2 with
284        | Values.Vundef -> Types.None
285        | Values.Vint (x2, x3) -> Types.None
286        | Values.Vnull ->
287          (match target with
288           | Csyntax.Tvoid -> Types.None
289           | Csyntax.Tint (tsz, tsg) ->
290             Types.Some (Values.Vint (tsz,
291               (BitVector.zero (AST.bitsize_of_intsize tsz))))
292           | Csyntax.Tpointer x2 -> Types.None
293           | Csyntax.Tarray (x2, x3) -> Types.None
294           | Csyntax.Tfunction (x2, x3) -> Types.None
295           | Csyntax.Tstruct (x2, x3) -> Types.None
296           | Csyntax.Tunion (x2, x3) -> Types.None
297           | Csyntax.Tcomp_ptr x2 -> Types.None)
298        | Values.Vptr x2 -> Types.None)
299     | Values.Vptr ptr1 ->
300       (match v2 with
301        | Values.Vundef -> Types.None
302        | Values.Vint (x2, x3) -> Types.None
303        | Values.Vnull -> Types.None
304        | Values.Vptr ptr2 ->
305          (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
306           | Bool.True ->
307             (match Nat.eqb (Csyntax.sizeof ty) Nat.O with
308              | Bool.True -> Types.None
309              | Bool.False ->
310                (match target with
311                 | Csyntax.Tvoid -> Types.None
312                 | Csyntax.Tint (tsz, tsg) ->
313                   (match Arithmetic.division_u (Nat.S (Nat.S (Nat.S (Nat.S
314                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
315                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
316                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
317                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
318                            Nat.O)))))))))))))))))))))))))))))))
319                            (Pointers.sub_offset (Nat.S (Nat.S (Nat.S (Nat.S
320                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
321                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
322                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
323                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
324                              (Nat.S (Nat.S (Nat.S (Nat.S
325                              Nat.O))))))))))))))))))))))))))))))))
326                              ptr1.Pointers.poff ptr2.Pointers.poff)
327                            (Integers.repr (Csyntax.sizeof ty)) with
328                    | Types.None -> Types.None
329                    | Types.Some v ->
330                      Types.Some (Values.Vint (tsz,
331                        (Arithmetic.zero_ext (Nat.S (Nat.S (Nat.S (Nat.S
332                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
333                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
334                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
335                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
336                          Nat.O))))))))))))))))))))))))))))))))
337                          (AST.bitsize_of_intsize tsz) v))))
338                 | Csyntax.Tpointer x2 -> Types.None
339                 | Csyntax.Tarray (x2, x3) -> Types.None
340                 | Csyntax.Tfunction (x2, x3) -> Types.None
341                 | Csyntax.Tstruct (x2, x3) -> Types.None
342                 | Csyntax.Tunion (x2, x3) -> Types.None
343                 | Csyntax.Tcomp_ptr x2 -> Types.None))
344           | Bool.False -> Types.None)))
345  | ClassifyOp.Sub_default (x, x0) -> Types.None
346
347(** val sem_mul :
348    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
349    Values.val0 Types.option **)
350let rec sem_mul v1 t1 v2 t2 =
351  match ClassifyOp.classify_aop t1 t2 with
352  | ClassifyOp.Aop_case_ii (x, x0) ->
353    (match v1 with
354     | Values.Vundef -> Types.None
355     | Values.Vint (sz1, n1) ->
356       (match v2 with
357        | Values.Vundef -> Types.None
358        | Values.Vint (sz2, n2) ->
359          AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
360            (sz2,
361            (Arithmetic.short_multiplication (AST.bitsize_of_intsize sz2) n10
362              n2)))) Types.None
363        | Values.Vnull -> Types.None
364        | Values.Vptr x1 -> Types.None)
365     | Values.Vnull -> Types.None
366     | Values.Vptr x1 -> Types.None)
367  | ClassifyOp.Aop_default (x, x0) -> Types.None
368
369(** val sem_div :
370    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
371    Values.val0 Types.option **)
372let rec sem_div v1 t1 v2 t2 =
373  match ClassifyOp.classify_aop t1 t2 with
374  | ClassifyOp.Aop_case_ii (x, sg) ->
375    (match v1 with
376     | Values.Vundef -> Types.None
377     | Values.Vint (sz1, n1) ->
378       (match v2 with
379        | Values.Vundef -> Types.None
380        | Values.Vint (sz2, n2) ->
381          (match sg with
382           | AST.Signed ->
383             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
384               Types.option_map (fun x0 -> Values.Vint (sz2, x0))
385                 (Arithmetic.division_s (AST.bitsize_of_intsize sz2) n10 n2))
386               Types.None
387           | AST.Unsigned ->
388             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
389               Types.option_map (fun x0 -> Values.Vint (sz2, x0))
390                 (Arithmetic.division_u
391                   (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
392                     Nat.O)))))))
393                     (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S
394                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
395                       Nat.O)))))))))) n10 n2)) Types.None)
396        | Values.Vnull -> Types.None
397        | Values.Vptr x0 -> Types.None)
398     | Values.Vnull -> Types.None
399     | Values.Vptr x0 -> Types.None)
400  | ClassifyOp.Aop_default (x, x0) -> Types.None
401
402(** val sem_mod :
403    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
404    Values.val0 Types.option **)
405let rec sem_mod v1 t1 v2 t2 =
406  match ClassifyOp.classify_aop t1 t2 with
407  | ClassifyOp.Aop_case_ii (sz, sg) ->
408    (match v1 with
409     | Values.Vundef -> Types.None
410     | Values.Vint (sz1, n1) ->
411       (match v2 with
412        | Values.Vundef -> Types.None
413        | Values.Vint (sz2, n2) ->
414          (match sg with
415           | AST.Signed ->
416             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
417               Types.option_map (fun x -> Values.Vint (sz2, x))
418                 (Arithmetic.modulus_s (AST.bitsize_of_intsize sz2) n10 n2))
419               Types.None
420           | AST.Unsigned ->
421             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
422               Types.option_map (fun x -> Values.Vint (sz2, x))
423                 (Arithmetic.modulus_u
424                   (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
425                     Nat.O)))))))
426                     (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S
427                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
428                       Nat.O)))))))))) n10 n2)) Types.None)
429        | Values.Vnull -> Types.None
430        | Values.Vptr x -> Types.None)
431     | Values.Vnull -> Types.None
432     | Values.Vptr x -> Types.None)
433  | ClassifyOp.Aop_default (x, x0) -> Types.None
434
435(** val sem_and : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
436let rec sem_and v1 v2 =
437  match v1 with
438  | Values.Vundef -> Types.None
439  | Values.Vint (sz1, n1) ->
440    (match v2 with
441     | Values.Vundef -> Types.None
442     | Values.Vint (sz2, n2) ->
443       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
444         (sz2,
445         (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2))))
446         Types.None
447     | Values.Vnull -> Types.None
448     | Values.Vptr x -> Types.None)
449  | Values.Vnull -> Types.None
450  | Values.Vptr x -> Types.None
451
452(** val sem_or : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
453let rec sem_or v1 v2 =
454  match v1 with
455  | Values.Vundef -> Types.None
456  | Values.Vint (sz1, n1) ->
457    (match v2 with
458     | Values.Vundef -> Types.None
459     | Values.Vint (sz2, n2) ->
460       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
461         (sz2,
462         (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
463           n2)))) Types.None
464     | Values.Vnull -> Types.None
465     | Values.Vptr x -> Types.None)
466  | Values.Vnull -> Types.None
467  | Values.Vptr x -> Types.None
468
469(** val sem_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
470let rec sem_xor v1 v2 =
471  match v1 with
472  | Values.Vundef -> Types.None
473  | Values.Vint (sz1, n1) ->
474    (match v2 with
475     | Values.Vundef -> Types.None
476     | Values.Vint (sz2, n2) ->
477       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
478         (sz2,
479         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
480           n2)))) Types.None
481     | Values.Vnull -> Types.None
482     | Values.Vptr x -> Types.None)
483  | Values.Vnull -> Types.None
484  | Values.Vptr x -> Types.None
485
486(** val sem_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
487let rec sem_shl v1 v2 =
488  match v1 with
489  | Values.Vundef -> Types.None
490  | Values.Vint (sz1, n1) ->
491    (match v2 with
492     | Values.Vundef -> Types.None
493     | Values.Vint (sz2, n2) ->
494       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
495                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
496                  (AST.bitsize_of_intsize sz1)) with
497        | Bool.True ->
498          Types.Some (Values.Vint (sz1,
499            (Vector.shift_left (AST.bitsize_of_intsize sz1)
500              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
501              n1 Bool.False)))
502        | Bool.False -> Types.None)
503     | Values.Vnull -> Types.None
504     | Values.Vptr x -> Types.None)
505  | Values.Vnull -> Types.None
506  | Values.Vptr x -> Types.None
507
508(** val sem_shr :
509    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
510    Values.val0 Types.option **)
511let rec sem_shr v1 t1 v2 t2 =
512  match ClassifyOp.classify_aop t1 t2 with
513  | ClassifyOp.Aop_case_ii (x, sg) ->
514    (match v1 with
515     | Values.Vundef -> Types.None
516     | Values.Vint (sz1, n1) ->
517       (match v2 with
518        | Values.Vundef -> Types.None
519        | Values.Vint (sz2, n2) ->
520          (match sg with
521           | AST.Signed ->
522             (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
523                      (Arithmetic.bitvector_of_nat
524                        (AST.bitsize_of_intsize sz2)
525                        (AST.bitsize_of_intsize sz1)) with
526              | Bool.True ->
527                Types.Some (Values.Vint (sz1,
528                  (Vector.shift_right
529                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
530                      (Nat.S Nat.O)))))))
531                      (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
532                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
533                        Nat.O))))))))))
534                    (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2)
535                      n2) n1
536                    (Vector.head'
537                      (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
538                        (Nat.S Nat.O)))))))
539                        (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
540                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
541                          Nat.O)))))))))) n1))))
542              | Bool.False -> Types.None)
543           | AST.Unsigned ->
544             (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
545                      (Arithmetic.bitvector_of_nat
546                        (AST.bitsize_of_intsize sz2)
547                        (AST.bitsize_of_intsize sz1)) with
548              | Bool.True ->
549                Types.Some (Values.Vint (sz1,
550                  (Vector.shift_right
551                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
552                      (Nat.S Nat.O)))))))
553                      (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
554                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
555                        Nat.O))))))))))
556                    (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2)
557                      n2) n1 Bool.False)))
558              | Bool.False -> Types.None))
559        | Values.Vnull -> Types.None
560        | Values.Vptr x0 -> Types.None)
561     | Values.Vnull -> Types.None
562     | Values.Vptr x0 -> Types.None)
563  | ClassifyOp.Aop_default (x, x0) -> Types.None
564
565(** val sem_cmp_mismatch :
566    Integers.comparison -> Values.val0 Types.option **)
567let rec sem_cmp_mismatch = function
568| Integers.Ceq -> Types.Some Values.vfalse
569| Integers.Cne -> Types.Some Values.vtrue
570| Integers.Clt -> Types.None
571| Integers.Cle -> Types.None
572| Integers.Cgt -> Types.None
573| Integers.Cge -> Types.None
574
575(** val sem_cmp_match : Integers.comparison -> Values.val0 Types.option **)
576let rec sem_cmp_match = function
577| Integers.Ceq -> Types.Some Values.vtrue
578| Integers.Cne -> Types.Some Values.vfalse
579| Integers.Clt -> Types.None
580| Integers.Cle -> Types.None
581| Integers.Cgt -> Types.None
582| Integers.Cge -> Types.None
583
584(** val sem_cmp :
585    Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
586    Csyntax.type0 -> GenMem.mem1 -> Values.val0 Types.option **)
587let rec sem_cmp c v1 t1 v2 t2 m =
588  match ClassifyOp.classify_cmp t1 t2 with
589  | ClassifyOp.Cmp_case_ii (x, sg) ->
590    (match v1 with
591     | Values.Vundef -> Types.None
592     | Values.Vint (sz1, n1) ->
593       (match v2 with
594        | Values.Vundef -> Types.None
595        | Values.Vint (sz2, n2) ->
596          (match sg with
597           | AST.Signed ->
598             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
599               (Values.of_bool
600                 (Values.cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)))
601               Types.None
602           | AST.Unsigned ->
603             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
604               (Values.of_bool
605                 (Values.cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)))
606               Types.None)
607        | Values.Vnull -> Types.None
608        | Values.Vptr x0 -> Types.None)
609     | Values.Vnull -> Types.None
610     | Values.Vptr x0 -> Types.None)
611  | ClassifyOp.Cmp_case_pp (x, x0) ->
612    (match v1 with
613     | Values.Vundef -> Types.None
614     | Values.Vint (x1, x2) -> Types.None
615     | Values.Vnull ->
616       (match v2 with
617        | Values.Vundef -> Types.None
618        | Values.Vint (x1, x2) -> Types.None
619        | Values.Vnull -> sem_cmp_match c
620        | Values.Vptr ptr2 -> sem_cmp_mismatch c)
621     | Values.Vptr ptr1 ->
622       (match v2 with
623        | Values.Vundef -> Types.None
624        | Values.Vint (x1, x2) -> Types.None
625        | Values.Vnull -> sem_cmp_mismatch c
626        | Values.Vptr ptr2 ->
627          (match Bool.andb (FrontEndMem.valid_pointer m ptr1)
628                   (FrontEndMem.valid_pointer m ptr2) with
629           | Bool.True ->
630             (match Pointers.eq_block ptr1.Pointers.pblock
631                      ptr2.Pointers.pblock with
632              | Bool.True ->
633                Types.Some
634                  (Values.of_bool
635                    (Values.cmp_offset c ptr1.Pointers.poff
636                      ptr2.Pointers.poff))
637              | Bool.False -> sem_cmp_mismatch c)
638           | Bool.False -> Types.None)))
639  | ClassifyOp.Cmp_default (x, x0) -> Types.None
640
641(** val cast_bool_to_target :
642    Csyntax.type0 -> Values.val0 Types.option -> Values.val0 Types.option **)
643let cast_bool_to_target ty = function
644| Types.None -> Types.None
645| Types.Some v ->
646  (match ty with
647   | Csyntax.Tvoid -> Types.None
648   | Csyntax.Tint (sz, sg) -> Types.Some (Values.zero_ext1 sz v)
649   | Csyntax.Tpointer x -> Types.None
650   | Csyntax.Tarray (x, x0) -> Types.None
651   | Csyntax.Tfunction (x, x0) -> Types.None
652   | Csyntax.Tstruct (x, x0) -> Types.None
653   | Csyntax.Tunion (x, x0) -> Types.None
654   | Csyntax.Tcomp_ptr x -> Types.None)
655
656(** val sem_unary_operation :
657    Csyntax.unary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
658    Types.option **)
659let sem_unary_operation op0 v ty =
660  match op0 with
661  | Csyntax.Onotbool -> sem_notbool v ty
662  | Csyntax.Onotint -> sem_notint v
663  | Csyntax.Oneg -> sem_neg v ty
664
665(** val sem_binary_operation :
666    Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
667    -> Csyntax.type0 -> GenMem.mem1 -> Csyntax.type0 -> Values.val0
668    Types.option **)
669let rec sem_binary_operation op0 v1 t1 v2 t2 m ty =
670  match op0 with
671  | Csyntax.Oadd -> sem_add v1 t1 v2 t2
672  | Csyntax.Osub -> sem_sub v1 t1 v2 t2 ty
673  | Csyntax.Omul -> sem_mul v1 t1 v2 t2
674  | Csyntax.Odiv -> sem_div v1 t1 v2 t2
675  | Csyntax.Omod -> sem_mod v1 t1 v2 t2
676  | Csyntax.Oand -> sem_and v1 v2
677  | Csyntax.Oor -> sem_or v1 v2
678  | Csyntax.Oxor -> sem_xor v1 v2
679  | Csyntax.Oshl -> sem_shl v1 v2
680  | Csyntax.Oshr -> sem_shr v1 t1 v2 t2
681  | Csyntax.Oeq ->
682    cast_bool_to_target ty (sem_cmp Integers.Ceq v1 t1 v2 t2 m)
683  | Csyntax.One0 ->
684    cast_bool_to_target ty (sem_cmp Integers.Cne v1 t1 v2 t2 m)
685  | Csyntax.Olt ->
686    cast_bool_to_target ty (sem_cmp Integers.Clt v1 t1 v2 t2 m)
687  | Csyntax.Ogt ->
688    cast_bool_to_target ty (sem_cmp Integers.Cgt v1 t1 v2 t2 m)
689  | Csyntax.Ole ->
690    cast_bool_to_target ty (sem_cmp Integers.Cle v1 t1 v2 t2 m)
691  | Csyntax.Oge ->
692    cast_bool_to_target ty (sem_cmp Integers.Cge v1 t1 v2 t2 m)
693
694(** val cast_int_int :
695    AST.intsize -> AST.signedness -> AST.intsize -> BitVector.bitVector ->
696    BitVector.bitVector **)
697let rec cast_int_int sz sg dstsz i =
698  match sg with
699  | AST.Signed ->
700    Arithmetic.sign_ext (AST.bitsize_of_intsize sz)
701      (AST.bitsize_of_intsize dstsz) i
702  | AST.Unsigned ->
703    Arithmetic.zero_ext (AST.bitsize_of_intsize sz)
704      (AST.bitsize_of_intsize dstsz) i
705
706type genv0 = Csyntax.clight_fundef Globalenvs.genv_t
707
708type env = Pointers.block Identifiers.identifier_map
709
710(** val empty_env : env **)
711let empty_env =
712  Identifiers.empty_map PreIdentifiers.SymbolTag
713
714(** val load_value_of_type :
715    Csyntax.type0 -> GenMem.mem1 -> Pointers.block -> Pointers.offset ->
716    Values.val0 Types.option **)
717let rec load_value_of_type ty m b ofs =
718  match Csyntax.access_mode ty with
719  | Csyntax.By_value chunk ->
720    FrontEndMem.loadv chunk m (Values.Vptr { Pointers.pblock = b;
721      Pointers.poff = ofs })
722  | Csyntax.By_reference ->
723    Types.Some (Values.Vptr { Pointers.pblock = b; Pointers.poff = ofs })
724  | Csyntax.By_nothing x -> Types.None
725
726(** val store_value_of_type :
727    Csyntax.type0 -> GenMem.mem1 -> Pointers.block -> Pointers.offset ->
728    Values.val0 -> GenMem.mem1 Types.option **)
729let rec store_value_of_type ty_dest m loc ofs v =
730  match Csyntax.access_mode ty_dest with
731  | Csyntax.By_value chunk ->
732    FrontEndMem.storev chunk m (Values.Vptr { Pointers.pblock = loc;
733      Pointers.poff = ofs }) v
734  | Csyntax.By_reference -> Types.None
735  | Csyntax.By_nothing x -> Types.None
736
737(** val blocks_of_env : env -> Pointers.block List.list **)
738let blocks_of_env e1 =
739  List.map (fun x -> x.Types.snd)
740    (Identifiers.elements PreIdentifiers.SymbolTag e1)
741
742(** val select_switch :
743    AST.intsize -> BitVector.bitVector -> Csyntax.labeled_statements ->
744    Csyntax.labeled_statements Types.option **)
745let rec select_switch sz n sl = match sl with
746| Csyntax.LSdefault x -> Types.Some sl
747| Csyntax.LScase (sz', c, s, sl') ->
748  AST.intsize_eq_elim sz sz' n (fun n0 ->
749    match BitVector.eq_bv (AST.bitsize_of_intsize sz') c n0 with
750    | Bool.True -> Types.Some sl
751    | Bool.False -> select_switch sz' n0 sl') Types.None
752
753(** val seq_of_labeled_statement :
754    Csyntax.labeled_statements -> Csyntax.statement **)
755let rec seq_of_labeled_statement = function
756| Csyntax.LSdefault s -> s
757| Csyntax.LScase (x, c, s, sl') ->
758  Csyntax.Ssequence (s, (seq_of_labeled_statement sl'))
759
760type cont =
761| Kstop
762| Kseq of Csyntax.statement * cont
763| Kwhile of Csyntax.expr * Csyntax.statement * cont
764| Kdowhile of Csyntax.expr * Csyntax.statement * cont
765| Kfor2 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
766| Kfor3 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
767| Kswitch of cont
768| Kcall of ((Pointers.block, Pointers.offset) Types.prod, Csyntax.type0)
769           Types.prod Types.option * Csyntax.function0 * env * cont
770
771(** val cont_rect_Type4 :
772    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
773    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
774    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
775    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
776    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
777    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
778    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
779    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
780let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
781| Kstop -> h_Kstop
782| Kseq (x_8622, x_8621) ->
783  h_Kseq x_8622 x_8621
784    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
785      h_Kswitch h_Kcall x_8621)
786| Kwhile (x_8625, x_8624, x_8623) ->
787  h_Kwhile x_8625 x_8624 x_8623
788    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
789      h_Kswitch h_Kcall x_8623)
790| Kdowhile (x_8628, x_8627, x_8626) ->
791  h_Kdowhile x_8628 x_8627 x_8626
792    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
793      h_Kswitch h_Kcall x_8626)
794| Kfor2 (x_8632, x_8631, x_8630, x_8629) ->
795  h_Kfor2 x_8632 x_8631 x_8630 x_8629
796    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
797      h_Kswitch h_Kcall x_8629)
798| Kfor3 (x_8636, x_8635, x_8634, x_8633) ->
799  h_Kfor3 x_8636 x_8635 x_8634 x_8633
800    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
801      h_Kswitch h_Kcall x_8633)
802| Kswitch x_8637 ->
803  h_Kswitch x_8637
804    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
805      h_Kswitch h_Kcall x_8637)
806| Kcall (x_8641, x_8640, x_8639, x_8638) ->
807  h_Kcall x_8641 x_8640 x_8639 x_8638
808    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
809      h_Kswitch h_Kcall x_8638)
810
811(** val cont_rect_Type3 :
812    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
813    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
814    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
815    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
816    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
817    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
818    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
819    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
820let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
821| Kstop -> h_Kstop
822| Kseq (x_8682, x_8681) ->
823  h_Kseq x_8682 x_8681
824    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
825      h_Kswitch h_Kcall x_8681)
826| Kwhile (x_8685, x_8684, x_8683) ->
827  h_Kwhile x_8685 x_8684 x_8683
828    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
829      h_Kswitch h_Kcall x_8683)
830| Kdowhile (x_8688, x_8687, x_8686) ->
831  h_Kdowhile x_8688 x_8687 x_8686
832    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
833      h_Kswitch h_Kcall x_8686)
834| Kfor2 (x_8692, x_8691, x_8690, x_8689) ->
835  h_Kfor2 x_8692 x_8691 x_8690 x_8689
836    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
837      h_Kswitch h_Kcall x_8689)
838| Kfor3 (x_8696, x_8695, x_8694, x_8693) ->
839  h_Kfor3 x_8696 x_8695 x_8694 x_8693
840    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
841      h_Kswitch h_Kcall x_8693)
842| Kswitch x_8697 ->
843  h_Kswitch x_8697
844    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
845      h_Kswitch h_Kcall x_8697)
846| Kcall (x_8701, x_8700, x_8699, x_8698) ->
847  h_Kcall x_8701 x_8700 x_8699 x_8698
848    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
849      h_Kswitch h_Kcall x_8698)
850
851(** val cont_rect_Type2 :
852    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
853    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
854    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
855    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
856    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
857    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
858    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
859    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
860let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
861| Kstop -> h_Kstop
862| Kseq (x_8712, x_8711) ->
863  h_Kseq x_8712 x_8711
864    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
865      h_Kswitch h_Kcall x_8711)
866| Kwhile (x_8715, x_8714, x_8713) ->
867  h_Kwhile x_8715 x_8714 x_8713
868    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
869      h_Kswitch h_Kcall x_8713)
870| Kdowhile (x_8718, x_8717, x_8716) ->
871  h_Kdowhile x_8718 x_8717 x_8716
872    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
873      h_Kswitch h_Kcall x_8716)
874| Kfor2 (x_8722, x_8721, x_8720, x_8719) ->
875  h_Kfor2 x_8722 x_8721 x_8720 x_8719
876    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
877      h_Kswitch h_Kcall x_8719)
878| Kfor3 (x_8726, x_8725, x_8724, x_8723) ->
879  h_Kfor3 x_8726 x_8725 x_8724 x_8723
880    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
881      h_Kswitch h_Kcall x_8723)
882| Kswitch x_8727 ->
883  h_Kswitch x_8727
884    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
885      h_Kswitch h_Kcall x_8727)
886| Kcall (x_8731, x_8730, x_8729, x_8728) ->
887  h_Kcall x_8731 x_8730 x_8729 x_8728
888    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
889      h_Kswitch h_Kcall x_8728)
890
891(** val cont_rect_Type1 :
892    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
893    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
894    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
895    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
896    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
897    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
898    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
899    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
900let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
901| Kstop -> h_Kstop
902| Kseq (x_8742, x_8741) ->
903  h_Kseq x_8742 x_8741
904    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
905      h_Kswitch h_Kcall x_8741)
906| Kwhile (x_8745, x_8744, x_8743) ->
907  h_Kwhile x_8745 x_8744 x_8743
908    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
909      h_Kswitch h_Kcall x_8743)
910| Kdowhile (x_8748, x_8747, x_8746) ->
911  h_Kdowhile x_8748 x_8747 x_8746
912    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
913      h_Kswitch h_Kcall x_8746)
914| Kfor2 (x_8752, x_8751, x_8750, x_8749) ->
915  h_Kfor2 x_8752 x_8751 x_8750 x_8749
916    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
917      h_Kswitch h_Kcall x_8749)
918| Kfor3 (x_8756, x_8755, x_8754, x_8753) ->
919  h_Kfor3 x_8756 x_8755 x_8754 x_8753
920    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
921      h_Kswitch h_Kcall x_8753)
922| Kswitch x_8757 ->
923  h_Kswitch x_8757
924    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
925      h_Kswitch h_Kcall x_8757)
926| Kcall (x_8761, x_8760, x_8759, x_8758) ->
927  h_Kcall x_8761 x_8760 x_8759 x_8758
928    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
929      h_Kswitch h_Kcall x_8758)
930
931(** val cont_rect_Type0 :
932    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
933    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
934    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
935    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
936    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
937    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
938    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
939    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
940let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
941| Kstop -> h_Kstop
942| Kseq (x_8772, x_8771) ->
943  h_Kseq x_8772 x_8771
944    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
945      h_Kswitch h_Kcall x_8771)
946| Kwhile (x_8775, x_8774, x_8773) ->
947  h_Kwhile x_8775 x_8774 x_8773
948    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
949      h_Kswitch h_Kcall x_8773)
950| Kdowhile (x_8778, x_8777, x_8776) ->
951  h_Kdowhile x_8778 x_8777 x_8776
952    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
953      h_Kswitch h_Kcall x_8776)
954| Kfor2 (x_8782, x_8781, x_8780, x_8779) ->
955  h_Kfor2 x_8782 x_8781 x_8780 x_8779
956    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
957      h_Kswitch h_Kcall x_8779)
958| Kfor3 (x_8786, x_8785, x_8784, x_8783) ->
959  h_Kfor3 x_8786 x_8785 x_8784 x_8783
960    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
961      h_Kswitch h_Kcall x_8783)
962| Kswitch x_8787 ->
963  h_Kswitch x_8787
964    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
965      h_Kswitch h_Kcall x_8787)
966| Kcall (x_8791, x_8790, x_8789, x_8788) ->
967  h_Kcall x_8791 x_8790 x_8789 x_8788
968    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
969      h_Kswitch h_Kcall x_8788)
970
971(** val cont_inv_rect_Type4 :
972    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
973    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
974    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
975    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
976    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
977    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
978    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
979    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
980    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
981let cont_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
982  let hcut = cont_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
983
984(** val cont_inv_rect_Type3 :
985    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
986    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
987    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
988    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
989    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
990    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
991    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
992    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
993    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
994let cont_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
995  let hcut = cont_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
996
997(** val cont_inv_rect_Type2 :
998    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
999    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1000    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1001    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1002    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1003    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1004    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1005    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1006    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1007let cont_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1008  let hcut = cont_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1009
1010(** val cont_inv_rect_Type1 :
1011    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
1012    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1013    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1014    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1015    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1016    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1017    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1018    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1019    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1020let cont_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1021  let hcut = cont_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1022
1023(** val cont_inv_rect_Type0 :
1024    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
1025    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1026    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1027    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1028    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1029    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1030    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1031    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1032    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1033let cont_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1034  let hcut = cont_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1035
1036(** val cont_discr : cont -> cont -> __ **)
1037let cont_discr x y =
1038  Logic.eq_rect_Type2 x
1039    (match x with
1040     | Kstop -> Obj.magic (fun _ dH -> dH)
1041     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1042     | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1043     | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1044     | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1045     | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1046     | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
1047     | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1048
1049(** val cont_jmdiscr : cont -> cont -> __ **)
1050let cont_jmdiscr x y =
1051  Logic.eq_rect_Type2 x
1052    (match x with
1053     | Kstop -> Obj.magic (fun _ dH -> dH)
1054     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1055     | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1056     | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1057     | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1058     | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1059     | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
1060     | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1061
1062(** val call_cont : cont -> cont **)
1063let rec call_cont k = match k with
1064| Kstop -> k
1065| Kseq (s, k0) -> call_cont k0
1066| Kwhile (e1, s, k0) -> call_cont k0
1067| Kdowhile (e1, s, k0) -> call_cont k0
1068| Kfor2 (e2, e3, s, k0) -> call_cont k0
1069| Kfor3 (e2, e3, s, k0) -> call_cont k0
1070| Kswitch k0 -> call_cont k0
1071| Kcall (x, x0, x1, x2) -> k
1072
1073type state0 =
1074| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem1
1075| Callstate of Values.val0 * Csyntax.clight_fundef * Values.val0 List.list
1076   * cont * GenMem.mem1
1077| Returnstate of Values.val0 * cont * GenMem.mem1
1078| Finalstate of Integers.int
1079
1080(** val state_rect_Type4 :
1081    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1082    'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
1083    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
1084    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
1085let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
1086| State (f, s, k, e1, m) -> h_State f s k e1 m
1087| Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
1088| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1089| Finalstate r -> h_Finalstate r
1090
1091(** val state_rect_Type5 :
1092    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1093    'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
1094    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
1095    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
1096let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
1097| State (f, s, k, e1, m) -> h_State f s k e1 m
1098| Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
1099| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1100| Finalstate r -> h_Finalstate r
1101
1102(** val state_rect_Type3 :
1103    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1104    'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
1105    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
1106    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
1107let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
1108| State (f, s, k, e1, m) -> h_State f s k e1 m
1109| Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
1110| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1111| Finalstate r -> h_Finalstate r
1112
1113(** val state_rect_Type2 :
1114    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1115    'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
1116    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
1117    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
1118let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
1119| State (f, s, k, e1, m) -> h_State f s k e1 m
1120| Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
1121| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1122| Finalstate r -> h_Finalstate r
1123
1124(** val state_rect_Type1 :
1125    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1126    'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
1127    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
1128    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
1129let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
1130| State (f, s, k, e1, m) -> h_State f s k e1 m
1131| Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
1132| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1133| Finalstate r -> h_Finalstate r
1134
1135(** val state_rect_Type0 :
1136    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1137    'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
1138    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
1139    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
1140let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
1141| State (f, s, k, e1, m) -> h_State f s k e1 m
1142| Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
1143| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1144| Finalstate r -> h_Finalstate r
1145
1146(** val state_inv_rect_Type4 :
1147    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1148    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
1149    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
1150    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
1151    -> 'a1) -> 'a1 **)
1152let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
1153  let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
1154
1155(** val state_inv_rect_Type3 :
1156    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1157    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
1158    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
1159    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
1160    -> 'a1) -> 'a1 **)
1161let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
1162  let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
1163
1164(** val state_inv_rect_Type2 :
1165    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1166    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
1167    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
1168    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
1169    -> 'a1) -> 'a1 **)
1170let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
1171  let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
1172
1173(** val state_inv_rect_Type1 :
1174    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1175    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
1176    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
1177    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
1178    -> 'a1) -> 'a1 **)
1179let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
1180  let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
1181
1182(** val state_inv_rect_Type0 :
1183    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1184    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
1185    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
1186    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
1187    -> 'a1) -> 'a1 **)
1188let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
1189  let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
1190
1191(** val state_discr : state0 -> state0 -> __ **)
1192let state_discr x y =
1193  Logic.eq_rect_Type2 x
1194    (match x with
1195     | State (a0, a1, a2, a3, a4) ->
1196       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1197     | Callstate (a0, a1, a2, a3, a4) ->
1198       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1199     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1200     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
1201
1202(** val state_jmdiscr : state0 -> state0 -> __ **)
1203let state_jmdiscr x y =
1204  Logic.eq_rect_Type2 x
1205    (match x with
1206     | State (a0, a1, a2, a3, a4) ->
1207       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1208     | Callstate (a0, a1, a2, a3, a4) ->
1209       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1210     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1211     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
1212
1213(** val find_label :
1214    Csyntax.label -> Csyntax.statement -> cont -> (Csyntax.statement, cont)
1215    Types.prod Types.option **)
1216let rec find_label lbl s k =
1217  match s with
1218  | Csyntax.Sskip -> Types.None
1219  | Csyntax.Sassign (x, x0) -> Types.None
1220  | Csyntax.Scall (x, x0, x1) -> Types.None
1221  | Csyntax.Ssequence (s1, s2) ->
1222    (match find_label lbl s1 (Kseq (s2, k)) with
1223     | Types.None -> find_label lbl s2 k
1224     | Types.Some sk -> Types.Some sk)
1225  | Csyntax.Sifthenelse (a, s1, s2) ->
1226    (match find_label lbl s1 k with
1227     | Types.None -> find_label lbl s2 k
1228     | Types.Some sk -> Types.Some sk)
1229  | Csyntax.Swhile (a, s1) -> find_label lbl s1 (Kwhile (a, s1, k))
1230  | Csyntax.Sdowhile (a, s1) -> find_label lbl s1 (Kdowhile (a, s1, k))
1231  | Csyntax.Sfor (a1, a2, a3, s1) ->
1232    (match find_label lbl a1 (Kseq ((Csyntax.Sfor (Csyntax.Sskip, a2, a3,
1233             s1)), k)) with
1234     | Types.None ->
1235       (match find_label lbl s1 (Kfor2 (a2, a3, s1, k)) with
1236        | Types.None -> find_label lbl a3 (Kfor3 (a2, a3, s1, k))
1237        | Types.Some sk -> Types.Some sk)
1238     | Types.Some sk -> Types.Some sk)
1239  | Csyntax.Sbreak -> Types.None
1240  | Csyntax.Scontinue -> Types.None
1241  | Csyntax.Sreturn x -> Types.None
1242  | Csyntax.Sswitch (e1, sl) -> find_label_ls lbl sl (Kswitch k)
1243  | Csyntax.Slabel (lbl', s') ->
1244    (match AST.ident_eq lbl lbl' with
1245     | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
1246     | Types.Inr _ -> find_label lbl s' k)
1247  | Csyntax.Sgoto x -> Types.None
1248  | Csyntax.Scost (c, s') -> find_label lbl s' k
1249(** val find_label_ls :
1250    Csyntax.label -> Csyntax.labeled_statements -> cont ->
1251    (Csyntax.statement, cont) Types.prod Types.option **)
1252and find_label_ls lbl sl k =
1253  match sl with
1254  | Csyntax.LSdefault s -> find_label lbl s k
1255  | Csyntax.LScase (x, x0, s, sl') ->
1256    (match find_label lbl s (Kseq ((seq_of_labeled_statement sl'), k)) with
1257     | Types.None -> find_label_ls lbl sl' k
1258     | Types.Some sk -> Types.Some sk)
1259
1260(** val fun_typeof : Csyntax.expr -> Csyntax.type0 **)
1261let fun_typeof e1 =
1262  match Csyntax.typeof e1 with
1263  | Csyntax.Tvoid -> Csyntax.Tvoid
1264  | Csyntax.Tint (a, b) -> Csyntax.Tint (a, b)
1265  | Csyntax.Tpointer ty -> ty
1266  | Csyntax.Tarray (a, b) -> Csyntax.Tarray (a, b)
1267  | Csyntax.Tfunction (a, b) -> Csyntax.Tfunction (a, b)
1268  | Csyntax.Tstruct (a, b) -> Csyntax.Tstruct (a, b)
1269  | Csyntax.Tunion (a, b) -> Csyntax.Tunion (a, b)
1270  | Csyntax.Tcomp_ptr a -> Csyntax.Tcomp_ptr a
1271
Note: See TracBrowser for help on using the repository browser.