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/Csyntax.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/Csyntax.v')
-rw-r--r-- | cfrontend/Csyntax.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index b332e216..f66b5bef 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -163,11 +163,13 @@ Definition typeof (e: expr) : type := (** ** Statements *) -(** Clight statements include all C statements except [goto] and labels. +(** Clight statements include all C statements. Only structured forms of [switch] are supported; moreover, the [default] case must occur last. Blocks and block-scoped declarations are not supported. *) +Definition label := ident. + Inductive statement : Type := | Sskip : statement (**r do nothing *) | Sassign : expr -> expr -> statement (**r assignment [lvalue = rvalue] *) @@ -181,6 +183,8 @@ Inductive statement : Type := | Scontinue : statement (**r [continue] statement *) | Sreturn : option expr -> statement (**r [return] statement *) | Sswitch : expr -> labeled_statements -> statement (**r [switch] statement *) + | Slabel : label -> statement -> statement + | Sgoto : label -> statement with labeled_statements : Type := (**r cases of a [switch] *) | LSdefault: statement -> labeled_statements @@ -447,6 +451,9 @@ type must be accessed: - [By_reference]: access by reference, i.e. by just returning the address of the variable; - [By_nothing]: no access is possible, e.g. for the [void] type. + +We currently do not support 64-bit integers and 128-bit floats, so these +have an access mode of [By_nothing]. *) Inductive mode: Type := |