From c48b9097201dc9a1e326acdbce491fe16cab01e6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 28 Aug 2007 12:57:58 +0000 Subject: Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csyntax.v | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) (limited to 'cfrontend/Csyntax.v') diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 3866669..31d1d87 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -136,15 +136,10 @@ with expr_descr : Set := | Ebinop: binary_operation -> expr -> expr -> expr_descr (**r binary operation *) | Ecast: type -> expr -> expr_descr (**r type cast ([(ty) e]) *) | Eindex: expr -> expr -> expr_descr (**r array indexing ([e1[e2]]) *) - | Ecall: expr -> exprlist -> expr_descr (**r function call *) | Eandbool: expr -> expr -> expr_descr (**r sequential and ([&&]) *) | Eorbool: expr -> expr -> expr_descr (**r sequential or ([||]) *) | Esizeof: type -> expr_descr (**r size of a type *) - | Efield: expr -> ident -> expr_descr (**r access to a member of a struct or union *) - -with exprlist : Set := - | Enil: exprlist - | Econs: expr -> exprlist -> exprlist. + | Efield: expr -> ident -> expr_descr. (**r access to a member of a struct or union *) (** Extract the type part of a type-annotated Clight expression. *) @@ -160,8 +155,8 @@ Definition typeof (e: expr) : type := Inductive statement : Set := | Sskip : statement (**r do nothing *) - | Sexpr : expr -> statement (**r evaluate expression for its side-effects *) | Sassign : expr -> expr -> statement (**r assignment [lvalue = rvalue] *) + | Scall: option expr -> expr -> list expr -> statement (**r function call *) | Ssequence : statement -> statement -> statement (**r sequence *) | Sifthenelse : expr -> statement -> statement -> statement (**r conditional *) | Swhile : expr -> statement -> statement (**r [while] loop *) -- cgit v1.2.3