Transition semantics for Clight and Csharpminor

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

1 files changed, 7 insertions, 0 deletions

diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index c03552c6..2bb9a9d4 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -120,6 +120,11 @@ Inductive wt_stmt: statement -> Prop :=
   | wt_Sswitch: forall e sl,
      wt_expr e -> wt_lblstmts sl ->
      wt_stmt (Sswitch e sl)
+  | wt_Slabel: forall lbl s,
+     wt_stmt s ->
+     wt_stmt (Slabel lbl s)
+  | wt_Sgoto: forall lbl,
+     wt_stmt (Sgoto lbl)
 
 with wt_lblstmts: labeled_statements -> Prop :=
   | wt_LSdefault: forall s,
@@ -362,6 +367,8 @@ Fixpoint typecheck_stmt (s: Csyntax.statement) {struct s} : bool :=
   | Csyntax.Sreturn (Some e) => typecheck_expr e
   | Csyntax.Sreturn None => true
   | Csyntax.Sswitch e sl => typecheck_expr e && typecheck_lblstmts sl
+  | Csyntax.Slabel lbl s => typecheck_stmt s
+  | Csyntax.Sgoto lbl => true
   end    
 
 with typecheck_lblstmts (sl: labeled_statements) {struct sl}: bool :=