diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-06-06 08:02:31 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-06-06 08:02:31 +0000 |
| commit | 37dc5ae288e8c2d857139751209575307f7913ad (patch) | |
| tree | 1733df35ced246355bde90a49d8d7c7273d96dff /backend/Cminorgen.v | |
| parent | 02d3c953c79af64a542ff659822fe003c0c532f3 (diff) | |
| download | compcert-37dc5ae288e8c2d857139751209575307f7913ad.tar.gz compcert-37dc5ae288e8c2d857139751209575307f7913ad.zip | |
Ajout Sswitch dans Csharpminor. Renommage type variable_info -> var_kind
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@35 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Cminorgen.v')
| -rw-r--r-- | backend/Cminorgen.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/backend/Cminorgen.v b/backend/Cminorgen.v index eeb7b7c8..e4c9a424 100644 --- a/backend/Cminorgen.v +++ b/backend/Cminorgen.v @@ -264,11 +264,12 @@ Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt) Some (Sblock ts) | Csharpminor.Sexit n => Some (Sexit n) + | Csharpminor.Sswitch e cases default => + do te <- transl_expr cenv e; Some(Sswitch te cases default) | Csharpminor.Sreturn None => Some (Sreturn None) | Csharpminor.Sreturn (Some e) => - do te <- transl_expr cenv e; - Some (Sreturn (Some te)) + do te <- transl_expr cenv e; Some (Sreturn (Some te)) end. (** Computation of the set of variables whose address is taken in @@ -314,6 +315,7 @@ Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := | Csharpminor.Sloop s => addr_taken_stmt s | Csharpminor.Sblock s => addr_taken_stmt s | Csharpminor.Sexit n => Identset.empty + | Csharpminor.Sswitch e cases default => addr_taken_expr e | Csharpminor.Sreturn None => Identset.empty | Csharpminor.Sreturn (Some e) => addr_taken_expr e end. @@ -326,7 +328,7 @@ Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := Definition assign_variable (atk: Identset.t) - (id_lv: ident * variable_info) + (id_lv: ident * var_kind) (cenv_stacksize: compilenv * Z) : compilenv * Z := let (cenv, stacksize) := cenv_stacksize in match id_lv with @@ -344,7 +346,7 @@ Definition assign_variable Fixpoint assign_variables (atk: Identset.t) - (id_lv_list: list (ident * variable_info)) + (id_lv_list: list (ident * var_kind)) (cenv_stacksize: compilenv * Z) {struct id_lv_list}: compilenv * Z := match id_lv_list with @@ -361,7 +363,7 @@ Definition build_compilenv (globenv, 0). Definition assign_global_variable - (ce: compilenv) (id_vi: ident * variable_info) : compilenv := + (ce: compilenv) (id_vi: ident * var_kind) : compilenv := match id_vi with | (id, Vscalar chunk) => PTree.set id (Var_global_scalar chunk) ce | (id, Varray sz) => PTree.set id Var_global_array ce |