source: extracted/csem.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 50.2 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Values
6
7open FrontEndVal
8
9open Hide
10
11open ByteValues
12
13open Division
14
15open Z
16
17open BitVectorZ
18
19open Pointers
20
21open GenMem
22
23open FrontEndMem
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open Extralib
32
33open Lists
34
35open Identifiers
36
37open Coqlib
38
39open Floats
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 Option
60
61open Setoids
62
63open Monad
64
65open Jmeq
66
67open Russell
68
69open Positive
70
71open Char
72
73open String
74
75open PreIdentifiers
76
77open Bool
78
79open Relations
80
81open Nat
82
83open List
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Types
94
95open Errors
96
97open Globalenvs
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 AST.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) (Identifiers.elements AST.symbolTag e1)
740
741(** val select_switch :
742    AST.intsize -> BitVector.bitVector -> Csyntax.labeled_statements ->
743    Csyntax.labeled_statements Types.option **)
744let rec select_switch sz n sl = match sl with
745| Csyntax.LSdefault x -> Types.Some sl
746| Csyntax.LScase (sz', c, s, sl') ->
747  AST.intsize_eq_elim sz sz' n (fun n0 ->
748    match BitVector.eq_bv (AST.bitsize_of_intsize sz') c n0 with
749    | Bool.True -> Types.Some sl
750    | Bool.False -> select_switch sz' n0 sl') Types.None
751
752(** val seq_of_labeled_statement :
753    Csyntax.labeled_statements -> Csyntax.statement **)
754let rec seq_of_labeled_statement = function
755| Csyntax.LSdefault s -> s
756| Csyntax.LScase (x, c, s, sl') ->
757  Csyntax.Ssequence (s, (seq_of_labeled_statement sl'))
758
759type cont =
760| Kstop
761| Kseq of Csyntax.statement * cont
762| Kwhile of Csyntax.expr * Csyntax.statement * cont
763| Kdowhile of Csyntax.expr * Csyntax.statement * cont
764| Kfor2 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
765| Kfor3 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
766| Kswitch of cont
767| Kcall of ((Pointers.block, Pointers.offset) Types.prod, Csyntax.type0)
768           Types.prod Types.option * Csyntax.function0 * env * cont
769
770(** val cont_rect_Type4 :
771    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
772    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
773    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
774    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
775    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
776    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
777    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
778    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
779let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
780| Kstop -> h_Kstop
781| Kseq (x_7621, x_7620) ->
782  h_Kseq x_7621 x_7620
783    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
784      h_Kswitch h_Kcall x_7620)
785| Kwhile (x_7624, x_7623, x_7622) ->
786  h_Kwhile x_7624 x_7623 x_7622
787    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
788      h_Kswitch h_Kcall x_7622)
789| Kdowhile (x_7627, x_7626, x_7625) ->
790  h_Kdowhile x_7627 x_7626 x_7625
791    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
792      h_Kswitch h_Kcall x_7625)
793| Kfor2 (x_7631, x_7630, x_7629, x_7628) ->
794  h_Kfor2 x_7631 x_7630 x_7629 x_7628
795    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
796      h_Kswitch h_Kcall x_7628)
797| Kfor3 (x_7635, x_7634, x_7633, x_7632) ->
798  h_Kfor3 x_7635 x_7634 x_7633 x_7632
799    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
800      h_Kswitch h_Kcall x_7632)
801| Kswitch x_7636 ->
802  h_Kswitch x_7636
803    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
804      h_Kswitch h_Kcall x_7636)
805| Kcall (x_7640, x_7639, x_7638, x_7637) ->
806  h_Kcall x_7640 x_7639 x_7638 x_7637
807    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
808      h_Kswitch h_Kcall x_7637)
809
810(** val cont_rect_Type3 :
811    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
812    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
813    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
814    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
815    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
816    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
817    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
818    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
819let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
820| Kstop -> h_Kstop
821| Kseq (x_7681, x_7680) ->
822  h_Kseq x_7681 x_7680
823    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
824      h_Kswitch h_Kcall x_7680)
825| Kwhile (x_7684, x_7683, x_7682) ->
826  h_Kwhile x_7684 x_7683 x_7682
827    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
828      h_Kswitch h_Kcall x_7682)
829| Kdowhile (x_7687, x_7686, x_7685) ->
830  h_Kdowhile x_7687 x_7686 x_7685
831    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
832      h_Kswitch h_Kcall x_7685)
833| Kfor2 (x_7691, x_7690, x_7689, x_7688) ->
834  h_Kfor2 x_7691 x_7690 x_7689 x_7688
835    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
836      h_Kswitch h_Kcall x_7688)
837| Kfor3 (x_7695, x_7694, x_7693, x_7692) ->
838  h_Kfor3 x_7695 x_7694 x_7693 x_7692
839    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
840      h_Kswitch h_Kcall x_7692)
841| Kswitch x_7696 ->
842  h_Kswitch x_7696
843    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
844      h_Kswitch h_Kcall x_7696)
845| Kcall (x_7700, x_7699, x_7698, x_7697) ->
846  h_Kcall x_7700 x_7699 x_7698 x_7697
847    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
848      h_Kswitch h_Kcall x_7697)
849
850(** val cont_rect_Type2 :
851    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
852    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
853    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
854    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
855    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
856    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
857    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
858    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
859let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
860| Kstop -> h_Kstop
861| Kseq (x_7711, x_7710) ->
862  h_Kseq x_7711 x_7710
863    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
864      h_Kswitch h_Kcall x_7710)
865| Kwhile (x_7714, x_7713, x_7712) ->
866  h_Kwhile x_7714 x_7713 x_7712
867    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
868      h_Kswitch h_Kcall x_7712)
869| Kdowhile (x_7717, x_7716, x_7715) ->
870  h_Kdowhile x_7717 x_7716 x_7715
871    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
872      h_Kswitch h_Kcall x_7715)
873| Kfor2 (x_7721, x_7720, x_7719, x_7718) ->
874  h_Kfor2 x_7721 x_7720 x_7719 x_7718
875    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
876      h_Kswitch h_Kcall x_7718)
877| Kfor3 (x_7725, x_7724, x_7723, x_7722) ->
878  h_Kfor3 x_7725 x_7724 x_7723 x_7722
879    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
880      h_Kswitch h_Kcall x_7722)
881| Kswitch x_7726 ->
882  h_Kswitch x_7726
883    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
884      h_Kswitch h_Kcall x_7726)
885| Kcall (x_7730, x_7729, x_7728, x_7727) ->
886  h_Kcall x_7730 x_7729 x_7728 x_7727
887    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
888      h_Kswitch h_Kcall x_7727)
889
890(** val cont_rect_Type1 :
891    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
892    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
893    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
894    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
895    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
896    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
897    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
898    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
899let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
900| Kstop -> h_Kstop
901| Kseq (x_7741, x_7740) ->
902  h_Kseq x_7741 x_7740
903    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
904      h_Kswitch h_Kcall x_7740)
905| Kwhile (x_7744, x_7743, x_7742) ->
906  h_Kwhile x_7744 x_7743 x_7742
907    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
908      h_Kswitch h_Kcall x_7742)
909| Kdowhile (x_7747, x_7746, x_7745) ->
910  h_Kdowhile x_7747 x_7746 x_7745
911    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
912      h_Kswitch h_Kcall x_7745)
913| Kfor2 (x_7751, x_7750, x_7749, x_7748) ->
914  h_Kfor2 x_7751 x_7750 x_7749 x_7748
915    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
916      h_Kswitch h_Kcall x_7748)
917| Kfor3 (x_7755, x_7754, x_7753, x_7752) ->
918  h_Kfor3 x_7755 x_7754 x_7753 x_7752
919    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
920      h_Kswitch h_Kcall x_7752)
921| Kswitch x_7756 ->
922  h_Kswitch x_7756
923    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
924      h_Kswitch h_Kcall x_7756)
925| Kcall (x_7760, x_7759, x_7758, x_7757) ->
926  h_Kcall x_7760 x_7759 x_7758 x_7757
927    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
928      h_Kswitch h_Kcall x_7757)
929
930(** val cont_rect_Type0 :
931    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
932    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
933    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
934    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
935    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
936    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
937    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
938    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
939let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
940| Kstop -> h_Kstop
941| Kseq (x_7771, x_7770) ->
942  h_Kseq x_7771 x_7770
943    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
944      h_Kswitch h_Kcall x_7770)
945| Kwhile (x_7774, x_7773, x_7772) ->
946  h_Kwhile x_7774 x_7773 x_7772
947    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
948      h_Kswitch h_Kcall x_7772)
949| Kdowhile (x_7777, x_7776, x_7775) ->
950  h_Kdowhile x_7777 x_7776 x_7775
951    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
952      h_Kswitch h_Kcall x_7775)
953| Kfor2 (x_7781, x_7780, x_7779, x_7778) ->
954  h_Kfor2 x_7781 x_7780 x_7779 x_7778
955    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
956      h_Kswitch h_Kcall x_7778)
957| Kfor3 (x_7785, x_7784, x_7783, x_7782) ->
958  h_Kfor3 x_7785 x_7784 x_7783 x_7782
959    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
960      h_Kswitch h_Kcall x_7782)
961| Kswitch x_7786 ->
962  h_Kswitch x_7786
963    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
964      h_Kswitch h_Kcall x_7786)
965| Kcall (x_7790, x_7789, x_7788, x_7787) ->
966  h_Kcall x_7790 x_7789 x_7788 x_7787
967    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
968      h_Kswitch h_Kcall x_7787)
969
970(** val cont_inv_rect_Type4 :
971    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
972    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
973    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
974    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
975    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
976    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
977    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
978    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
979    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
980let cont_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
981  let hcut = cont_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
982
983(** val cont_inv_rect_Type3 :
984    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
985    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
986    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
987    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
988    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
989    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
990    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
991    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
992    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
993let cont_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
994  let hcut = cont_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
995
996(** val cont_inv_rect_Type2 :
997    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
998    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
999    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1000    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1001    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1002    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1003    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1004    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1005    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1006let cont_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1007  let hcut = cont_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1008
1009(** val cont_inv_rect_Type1 :
1010    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
1011    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1012    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1013    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1014    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1015    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1016    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1017    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1018    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1019let cont_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1020  let hcut = cont_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1021
1022(** val cont_inv_rect_Type0 :
1023    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
1024    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1025    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1026    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1027    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1028    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1029    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1030    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1031    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1032let cont_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1033  let hcut = cont_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1034
1035(** val cont_discr : cont -> cont -> __ **)
1036let cont_discr x y =
1037  Logic.eq_rect_Type2 x
1038    (match x with
1039     | Kstop -> Obj.magic (fun _ dH -> dH)
1040     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1041     | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1042     | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1043     | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1044     | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1045     | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
1046     | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1047
1048(** val cont_jmdiscr : cont -> cont -> __ **)
1049let cont_jmdiscr x y =
1050  Logic.eq_rect_Type2 x
1051    (match x with
1052     | Kstop -> Obj.magic (fun _ dH -> dH)
1053     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1054     | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1055     | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1056     | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1057     | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1058     | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
1059     | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1060
1061(** val call_cont : cont -> cont **)
1062let rec call_cont k = match k with
1063| Kstop -> k
1064| Kseq (s, k0) -> call_cont k0
1065| Kwhile (e1, s, k0) -> call_cont k0
1066| Kdowhile (e1, s, k0) -> call_cont k0
1067| Kfor2 (e2, e3, s, k0) -> call_cont k0
1068| Kfor3 (e2, e3, s, k0) -> call_cont k0
1069| Kswitch k0 -> call_cont k0
1070| Kcall (x, x0, x1, x2) -> k
1071
1072type state0 =
1073| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem1
1074| Callstate of Csyntax.clight_fundef * Values.val0 List.list * cont
1075   * GenMem.mem1
1076| Returnstate of Values.val0 * cont * GenMem.mem1
1077| Finalstate of Integers.int
1078
1079(** val state_rect_Type4 :
1080    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1081    'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
1082    GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
1083    (Integers.int -> 'a1) -> state0 -> 'a1 **)
1084let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
1085| State (f, s, k, e1, m) -> h_State f s k e1 m
1086| Callstate (fd, args, k, m) -> h_Callstate fd args k m
1087| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1088| Finalstate r -> h_Finalstate r
1089
1090(** val state_rect_Type5 :
1091    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1092    'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
1093    GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
1094    (Integers.int -> 'a1) -> state0 -> 'a1 **)
1095let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
1096| State (f, s, k, e1, m) -> h_State f s k e1 m
1097| Callstate (fd, args, k, m) -> h_Callstate fd args k m
1098| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1099| Finalstate r -> h_Finalstate r
1100
1101(** val state_rect_Type3 :
1102    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1103    'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
1104    GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
1105    (Integers.int -> 'a1) -> state0 -> 'a1 **)
1106let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
1107| State (f, s, k, e1, m) -> h_State f s k e1 m
1108| Callstate (fd, args, k, m) -> h_Callstate fd args k m
1109| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1110| Finalstate r -> h_Finalstate r
1111
1112(** val state_rect_Type2 :
1113    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1114    'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
1115    GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
1116    (Integers.int -> 'a1) -> state0 -> 'a1 **)
1117let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
1118| State (f, s, k, e1, m) -> h_State f s k e1 m
1119| Callstate (fd, args, k, m) -> h_Callstate fd args k m
1120| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1121| Finalstate r -> h_Finalstate r
1122
1123(** val state_rect_Type1 :
1124    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1125    'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
1126    GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
1127    (Integers.int -> 'a1) -> state0 -> 'a1 **)
1128let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
1129| State (f, s, k, e1, m) -> h_State f s k e1 m
1130| Callstate (fd, args, k, m) -> h_Callstate fd args k m
1131| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1132| Finalstate r -> h_Finalstate r
1133
1134(** val state_rect_Type0 :
1135    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1136    'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
1137    GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
1138    (Integers.int -> 'a1) -> state0 -> 'a1 **)
1139let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
1140| State (f, s, k, e1, m) -> h_State f s k e1 m
1141| Callstate (fd, args, k, m) -> h_Callstate fd args k m
1142| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1143| Finalstate r -> h_Finalstate r
1144
1145(** val state_inv_rect_Type4 :
1146    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1147    GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
1148    List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
1149    GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1150let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
1151  let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
1152
1153(** val state_inv_rect_Type3 :
1154    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1155    GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
1156    List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
1157    GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1158let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
1159  let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
1160
1161(** val state_inv_rect_Type2 :
1162    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1163    GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
1164    List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
1165    GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1166let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
1167  let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
1168
1169(** val state_inv_rect_Type1 :
1170    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1171    GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
1172    List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
1173    GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1174let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
1175  let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
1176
1177(** val state_inv_rect_Type0 :
1178    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1179    GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
1180    List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
1181    GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1182let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
1183  let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
1184
1185(** val state_discr : state0 -> state0 -> __ **)
1186let state_discr x y =
1187  Logic.eq_rect_Type2 x
1188    (match x with
1189     | State (a0, a1, a2, a3, a4) ->
1190       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1191     | Callstate (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1192     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1193     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
1194
1195(** val state_jmdiscr : state0 -> state0 -> __ **)
1196let state_jmdiscr x y =
1197  Logic.eq_rect_Type2 x
1198    (match x with
1199     | State (a0, a1, a2, a3, a4) ->
1200       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1201     | Callstate (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1202     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1203     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
1204
1205(** val find_label :
1206    Csyntax.label -> Csyntax.statement -> cont -> (Csyntax.statement, cont)
1207    Types.prod Types.option **)
1208let rec find_label lbl s k =
1209  match s with
1210  | Csyntax.Sskip -> Types.None
1211  | Csyntax.Sassign (x, x0) -> Types.None
1212  | Csyntax.Scall (x, x0, x1) -> Types.None
1213  | Csyntax.Ssequence (s1, s2) ->
1214    (match find_label lbl s1 (Kseq (s2, k)) with
1215     | Types.None -> find_label lbl s2 k
1216     | Types.Some sk -> Types.Some sk)
1217  | Csyntax.Sifthenelse (a, s1, s2) ->
1218    (match find_label lbl s1 k with
1219     | Types.None -> find_label lbl s2 k
1220     | Types.Some sk -> Types.Some sk)
1221  | Csyntax.Swhile (a, s1) -> find_label lbl s1 (Kwhile (a, s1, k))
1222  | Csyntax.Sdowhile (a, s1) -> find_label lbl s1 (Kdowhile (a, s1, k))
1223  | Csyntax.Sfor (a1, a2, a3, s1) ->
1224    (match find_label lbl a1 (Kseq ((Csyntax.Sfor (Csyntax.Sskip, a2, a3,
1225             s1)), k)) with
1226     | Types.None ->
1227       (match find_label lbl s1 (Kfor2 (a2, a3, s1, k)) with
1228        | Types.None -> find_label lbl a3 (Kfor3 (a2, a3, s1, k))
1229        | Types.Some sk -> Types.Some sk)
1230     | Types.Some sk -> Types.Some sk)
1231  | Csyntax.Sbreak -> Types.None
1232  | Csyntax.Scontinue -> Types.None
1233  | Csyntax.Sreturn x -> Types.None
1234  | Csyntax.Sswitch (e1, sl) -> find_label_ls lbl sl (Kswitch k)
1235  | Csyntax.Slabel (lbl', s') ->
1236    (match AST.ident_eq lbl lbl' with
1237     | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
1238     | Types.Inr _ -> find_label lbl s' k)
1239  | Csyntax.Sgoto x -> Types.None
1240  | Csyntax.Scost (c, s') -> find_label lbl s' k
1241(** val find_label_ls :
1242    Csyntax.label -> Csyntax.labeled_statements -> cont ->
1243    (Csyntax.statement, cont) Types.prod Types.option **)
1244and find_label_ls lbl sl k =
1245  match sl with
1246  | Csyntax.LSdefault s -> find_label lbl s k
1247  | Csyntax.LScase (x, x0, s, sl') ->
1248    (match find_label lbl s (Kseq ((seq_of_labeled_statement sl'), k)) with
1249     | Types.None -> find_label_ls lbl sl' k
1250     | Types.Some sk -> Types.Some sk)
1251
1252(** val fun_typeof : Csyntax.expr -> Csyntax.type0 **)
1253let fun_typeof e1 =
1254  match Csyntax.typeof e1 with
1255  | Csyntax.Tvoid -> Csyntax.Tvoid
1256  | Csyntax.Tint (a, b) -> Csyntax.Tint (a, b)
1257  | Csyntax.Tpointer ty -> ty
1258  | Csyntax.Tarray (a, b) -> Csyntax.Tarray (a, b)
1259  | Csyntax.Tfunction (a, b) -> Csyntax.Tfunction (a, b)
1260  | Csyntax.Tstruct (a, b) -> Csyntax.Tstruct (a, b)
1261  | Csyntax.Tunion (a, b) -> Csyntax.Tunion (a, b)
1262  | Csyntax.Tcomp_ptr a -> Csyntax.Tcomp_ptr a
1263
Note: See TracBrowser for help on using the repository browser.