1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
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. *)
14 (* *********************************************************************)
16 (* Generic program transformation *)
22 (* Recording fresh temporaries *)
24 let temporaries = ref ([]: decl list)
29 let new_temp_var ?(name = "t") ty =
30 let id = Env.fresh_ident name in
31 temporaries := (Storage_default, id, ty, None) :: !temporaries;
34 let new_temp ?(name = "t") ty =
35 let id = new_temp_var ~name ty in
36 { edesc = EVar id; etyp = ty }
39 let temps = !temporaries in
43 (* Generic transformation *)
46 ?(decl = fun env d -> d)
47 ?(fundef = fun env fd -> fd)
48 ?(composite = fun env su id fl -> fl)
49 ?(typedef = fun env id ty -> ty)
52 (* In all transformations of interest so far, the environment is used only
53 for its type definitions and struct/union definitions,
54 so we do not update it for other definitions. *)
56 let rec transf_globdecls env accu = function
61 | Gdecl((sto, id, ty, init) as d) ->
62 (Gdecl(decl env d), Env.add_ident env id sto ty)
64 (Gfundef(fundef env f),
65 Env.add_ident env f.fd_name f.fd_storage (fundef_typ f))
66 | Gcompositedecl(su, id) ->
67 (Gcompositedecl(su, id),
68 Env.add_composite env id (composite_info_decl env su))
69 | Gcompositedef(su, id, fl) ->
70 (Gcompositedef(su, id, composite env su id fl),
71 Env.add_composite env id (composite_info_def env su fl))
73 (Gtypedef(id, typedef env id ty), Env.add_typedef env id ty)
74 | Genumdef _ as gd -> (gd, env)
75 | Gpragma _ as gd -> (gd, env)
77 transf_globdecls env' ({g with gdesc = desc'} :: accu) gl
79 in transf_globdecls (Builtins.environment()) [] p