source: driver/extracted/fresh.ml @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 2.1 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77(** val max_id : AST.ident -> AST.ident -> AST.ident **)
78let max_id a b =
79  let a0 = a in let b0 = b in Positive.max a0 b0
80
81(** val max_id_of_env :
82    (AST.ident, Csyntax.type0) Types.prod List.list -> AST.ident **)
83let max_id_of_env =
84  List.foldr (fun it id -> max_id it.Types.fst id) Positive.One
85
86(** val max_id_of_fn : Csyntax.function0 -> AST.ident **)
87let max_id_of_fn f =
88  max_id_of_env (List.append f.Csyntax.fn_params f.Csyntax.fn_vars)
89
90(** val max_id_of_fundef : Csyntax.clight_fundef -> AST.ident **)
91let max_id_of_fundef = function
92| Csyntax.CL_Internal f0 -> max_id_of_fn f0
93| Csyntax.CL_External (id, x, x0) -> id
94
95(** val max_id_of_functs :
96    (AST.ident, Csyntax.clight_fundef) Types.prod List.list -> AST.ident **)
97let max_id_of_functs =
98  List.foldr (fun idf id ->
99    max_id (max_id idf.Types.fst (max_id_of_fundef idf.Types.snd)) id)
100    Positive.One
101
102(** val max_id_of_globvars :
103    ((AST.ident, AST.region) Types.prod, (AST.init_data List.list,
104    Csyntax.type0) Types.prod) Types.prod List.list -> AST.ident **)
105let max_id_of_globvars =
106  List.foldr (fun it id -> max_id it.Types.fst.Types.fst id) Positive.One
107
108(** val max_id_of_program : Csyntax.clight_program -> AST.ident **)
109let max_id_of_program p =
110  max_id (max_id (max_id_of_functs p.AST.prog_funct) p.AST.prog_main)
111    (max_id_of_globvars p.AST.prog_vars)
112
113(** val universe_of_max : AST.ident -> Identifiers.universe **)
114let universe_of_max mx =
115  let i = mx in let next = Positive.succ i in next
116
117(** val universe_for_program :
118    Csyntax.clight_program -> Identifiers.universe **)
119let universe_for_program p =
120  universe_of_max (max_id_of_program p)
121
Note: See TracBrowser for help on using the repository browser.