Ajout construction Sswitch dans Cminor

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@31 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 13 insertions, 0 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index 54d5552..826c529 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -59,6 +59,7 @@ Inductive stmt : Set :=
   | Sloop: stmt -> stmt
   | Sblock: stmt -> stmt
   | Sexit: nat -> stmt
+  | Sswitch: expr -> list (int * nat) -> nat -> stmt
   | Sreturn: option expr -> stmt.
 
 (** Functions are composed of a signature, a list of parameter names,
@@ -106,6 +107,13 @@ Definition outcome_block (out: outcome) : outcome :=
   | Out_return optv => Out_return optv
   end.
 
+Fixpoint switch_target (n: int) (dfl: nat) (cases: list (int * nat))
+                       {struct cases} : nat :=
+  match cases with
+  | nil => dfl
+  | (n1, lbl1) :: rem => if Int.eq n n1 then lbl1 else switch_target n dfl rem
+  end.
+
 (** Three kinds of evaluation environments are involved:
 - [genv]: global environments, define symbols and functions;
 - [env]: local environments, map local variables to values;
@@ -310,6 +318,11 @@ with exec_stmt:
   | exec_Sexit:
       forall sp e m n,
       exec_stmt sp e m (Sexit n) e m (Out_exit n)
+  | exec_Sswitch:
+      forall sp e m a cases default e1 m1 n,
+      eval_expr sp nil e m a e1 m1 (Vint n) ->
+      exec_stmt sp e m (Sswitch a cases default)
+                   e1 m1 (Out_exit (switch_target n default cases))
   | exec_Sreturn_none:
       forall sp e m,
       exec_stmt sp e m (Sreturn None) e m (Out_return None)