From 213bf38509f4f92545d4c5749c25a55b9a9dda36 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 3 Aug 2009 15:32:27 +0000 Subject: Transition semantics for Clight and Csharpminor git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csyntax.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'cfrontend/Csyntax.v') diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index b332e21..f66b5be 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 := -- cgit v1.2.3