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/Csyntax.v | 17 +---------------- 1 file changed, 1 insertion(+), 16 deletions(-) (limited to 'cfrontend/Csyntax.v') diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index d3bd8d6f..979d0bca 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -130,11 +130,7 @@ Inductive fundef : Set := (** Program *) -Record program : Set := mkprogram { - prog_funct: list (ident * fundef); - prog_defs: list (ident * type * list init_data); - prog_main: ident -}. +Definition program : Set := AST.program fundef type. (** ** Operations over types *) @@ -293,17 +289,6 @@ Definition access_mode (ty: type) : mode := | Tunion fList => By_nothing end. -(** Conversion of a Clight program into an AST program *) - -Definition extract_global_var (id_ty_init: ident * type * list init_data) := - match id_ty_init with (id, ty, init) => (id, init) end. - -Definition program_of_program (p: program) : AST.program fundef := - AST.mkprogram - p.(prog_funct) - p.(prog_main) - (List.map extract_global_var p.(prog_defs)). - (** Classification of arithmetic operations and comparisons *) Inductive classify_add_cases : Set := -- cgit