]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blob - cparser/Builtins.ml
Control and copyright added.
[pkg-cerco/acc-trusted.git] / cparser / Builtins.ml
1 (* *********************************************************************)
2 (*                                                                     *)
3 (*              The Compcert verified compiler                         *)
4 (*                                                                     *)
5 (*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6 (*                                                                     *)
7 (*  Copyright Institut National de Recherche en Informatique et en     *)
8 (*  Automatique.  All rights reserved.  This file is distributed       *)
9 (*  under the terms of the GNU General Public License as published by  *)
10 (*  the Free Software Foundation, either version 2 of the License, or  *)
11 (*  (at your option) any later version.  This file is also distributed *)
12 (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13 (*                                                                     *)
14 (* *********************************************************************)
15
16 (* Compiler built-ins *)
17
18 open C
19 open Cutil
20
21 let env = ref Env.empty
22 let idents = ref []
23 let decls = ref []
24
25 let environment () = !env
26 let identifiers () = !idents
27 let declarations () = List.rev !decls
28
29 let add_typedef (s, ty) =
30   let (id, env') = Env.enter_typedef !env s ty in
31   env := env';
32   idents := id :: !idents;
33   decls := {gdesc = Gtypedef(id, ty); gloc = no_loc} :: !decls
34
35 let add_function (s, (res, args, va)) =
36   let ty =
37     TFun(res,
38          Some (List.map (fun ty -> (Env.fresh_ident "", ty)) args),
39          va, []) in
40   let (id, env') = Env.enter_ident !env s Storage_extern ty in
41   env := env';
42   idents := id :: !idents;
43   decls := {gdesc = Gdecl(Storage_extern, id, ty, None); gloc = no_loc} :: !decls
44
45 type t = {
46   typedefs: (string * C.typ) list;
47   functions: (string * (C.typ * C.typ list * bool)) list
48 }
49
50 let set blt =
51   env := Env.empty;
52   idents := [];
53   List.iter add_typedef blt.typedefs;
54   List.iter add_function blt.functions