From 6c0511a03c8c970435d8b97e600312ac45340801 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 5 Sep 2006 12:32:59 +0000 Subject: Revu traitement des variables globales dans AST.program et dans Globalenvs. Adaptation frontend, backend en consequence. Integration passe C -> C#minor dans common/Main.v. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@77 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgen.v | 21 ++++++--------------- 1 file changed, 6 insertions(+), 15 deletions(-) (limited to 'cfrontend/Cshmgen.v') diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 58c0bb8..5585416 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -562,8 +562,10 @@ with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt) (*** Translation of functions *) -Definition transl_params := transf_partial_program chunk_of_type. -Definition transl_vars := transf_partial_program var_kind_of_type. +Definition transl_params (l: list (ident * type)) := + AST.map_partial chunk_of_type l. +Definition transl_vars (l: list (ident * type)) := + AST.map_partial var_kind_of_type l. Definition transl_function (f: Csyntax.function) : option function := do tparams <- transl_params (Csyntax.fn_params f); @@ -581,18 +583,7 @@ Definition transl_fundef (f: Csyntax.fundef) : option fundef := (** ** Translation of programs *) -Fixpoint transl_global_vars - (vl: list (ident * type * list init_data)) : - option (list (ident * var_kind * list init_data)) := - match vl with - | nil => Some nil - | (id, ty, init) :: rem => - do vk <- var_kind_of_type ty; - do trem <- transl_global_vars rem; - Some ((id, vk, init) :: trem) - end. +Definition transl_globvar (ty: type) := var_kind_of_type ty. Definition transl_program (p: Csyntax.program) : option program := - do tfun <- transf_partial_program transl_fundef (Csyntax.prog_funct p); - do tvars <- transl_global_vars (Csyntax.prog_defs p); - Some (mkprogram tfun (Csyntax.prog_main p) tvars). + transform_partial_program2 transl_fundef transl_globvar p. -- cgit v1.2.3