diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-05 12:32:59 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-05 12:32:59 +0000 |
commit | 6c0511a03c8c970435d8b97e600312ac45340801 (patch) | |
tree | d42b16c8f77d1aa34e570647eb6728a4a9f4e72b /cfrontend/Csyntax.v | |
parent | 81afbd38d1597cefc03dd699fd115c4261c6877f (diff) | |
download | compcert-6c0511a03c8c970435d8b97e600312ac45340801.tar.gz compcert-6c0511a03c8c970435d8b97e600312ac45340801.zip |
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
Diffstat (limited to 'cfrontend/Csyntax.v')
-rw-r--r-- | cfrontend/Csyntax.v | 17 |
1 files changed, 1 insertions, 16 deletions
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 := |