diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-03 15:32:27 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-03 15:32:27 +0000 |
commit | 213bf38509f4f92545d4c5749c25a55b9a9dda36 (patch) | |
tree | a40df8011ab5fabb0de362befc53e7af164c70ae /cfrontend/Ctyping.v | |
parent | 88b98f00facde51bff705a3fb6c32a73937428cb (diff) | |
download | compcert-213bf38509f4f92545d4c5749c25a55b9a9dda36.tar.gz compcert-213bf38509f4f92545d4c5749c25a55b9a9dda36.zip |
Transition semantics for Clight and Csharpminor
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Ctyping.v')
-rw-r--r-- | cfrontend/Ctyping.v | 7 |
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 := |