diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
commit | c48b9097201dc9a1e326acdbce491fe16cab01e6 (patch) | |
tree | 53335d9dcb4aead3ec1f42e4138e87649640edd0 /cfrontend/Csyntax.v | |
parent | 2b89ae94ffb6dc56fa780acced8ab7ad0afbb3b5 (diff) |
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
Diffstat (limited to 'cfrontend/Csyntax.v')
-rw-r--r-- | cfrontend/Csyntax.v | 9 |
1 files changed, 2 insertions, 7 deletions
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 *) |