diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-07-02 14:55:31 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-07-17 09:17:28 +0200 |
| commit | fb20aab431a768299118ed30822af59cab13325e (patch) | |
| tree | 032ece0aa8bab2d9932b91056fbf0731fd72cf45 /cfrontend/C2C.ml | |
| parent | 8b0de52ffa302298abe8d0d6e3b6ed339a2354ba (diff) | |
| download | compcert-kvx-fb20aab431a768299118ed30822af59cab13325e.tar.gz compcert-kvx-fb20aab431a768299118ed30822af59cab13325e.zip | |
Remove the cparser/Builtins module
Move its definitions to modules C (the type `builtins`) and Env
(the operations that deal with the initial environment).
Reasons for the refactoring:
1- The name "Builtins" will soon be reused for a Coq module
2- `Env.initial()` makes more sense than `Builtins.environment()`.
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index b81bd022..4d0e52e1 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -155,8 +155,8 @@ let ais_annot_functions = [] let builtins_generic = { - Builtins.typedefs = []; - Builtins.functions = + builtin_typedefs = []; + builtin_functions = ais_annot_functions @ [ @@ -300,9 +300,12 @@ let builtins_generic = { (* Add processor-dependent builtins *) -let builtins = - Builtins.({ typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; - functions = builtins_generic.Builtins.functions @ CBuiltins.builtins.functions }) +let builtins = { + builtin_typedefs = + builtins_generic.builtin_typedefs @ CBuiltins.builtins.builtin_typedefs; + builtin_functions = + builtins_generic.builtin_functions @ CBuiltins.builtins.builtin_functions +} (** ** The known attributes *) @@ -1233,7 +1236,7 @@ let convertFundecl env (sto, id, ty, optinit) = if id.name = "free" then AST.EF_free else if Str.string_match re_runtime id.name 0 then AST.EF_runtime(id'', sg) else if Str.string_match re_builtin id.name 0 - && List.mem_assoc id.name builtins.Builtins.functions + && List.mem_assoc id.name builtins.builtin_functions then AST.EF_builtin(id'', sg) else AST.EF_external(id'', sg) in (id', AST.Gfun(Ctypes.External(ef, args, res, cconv))) @@ -1432,7 +1435,7 @@ let convertProgram p = Hashtbl.clear decl_atom; Hashtbl.clear stringTable; Hashtbl.clear wstringTable; - let p = cleanupGlobals (Builtins.declarations() @ p) in + let p = cleanupGlobals (Env.initial_declarations() @ p) in try let env = translEnv Env.empty p in let typs = convertCompositedefs env [] p in |