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

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 *)