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, 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 :=