Clight: ajout Econdition, suppression Eindex.

caml/PrintCsyntax.ml: afficher les formes a[b] et a->fld.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@789 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 37 insertions, 17 deletions

diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index a25c5b8b..75dbc145 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -482,7 +482,7 @@ Definition eval_exprlist_prop (al: list Csyntax.expr) (vl: list val) : Prop :=
     (TR: transl_exprlist al = OK tal),
   Csharpminor.eval_exprlist tprog te m tal vl.
 
-(* Check (eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop).*)
+(* Check (eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop). *)
 
 Lemma transl_Econst_int_correct:
   forall (i : int) (ty : type),
@@ -565,6 +565,38 @@ Proof.
   eapply transl_binop_correct; eauto. 
 Qed.
 
+Lemma transl_Econdition_true_correct:
+  forall (a1 a2 a3 : Csyntax.expr) (ty : type) (v1 v2 : val),
+  Csem.eval_expr ge e m a1 v1 ->
+  eval_expr_prop a1 v1 ->
+  is_true v1 (typeof a1) ->
+  Csem.eval_expr ge e m a2 v2 ->
+  eval_expr_prop a2 v2 ->
+  eval_expr_prop (Expr (Csyntax.Econdition a1 a2 a3) ty) v2.
+Proof.
+  intros; red; intros. inv WT. monadInv TR. 
+  exploit make_boolean_correct_true. eapply H0; eauto. eauto.
+  intros [vb [EVAL ISTRUE]].
+  eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto.
+  simpl. eauto. 
+Qed.
+
+Lemma transl_Econdition_false_correct:
+  forall (a1 a2 a3 : Csyntax.expr) (ty : type) (v1 v3 : val),
+  Csem.eval_expr ge e m a1 v1 ->
+  eval_expr_prop a1 v1 ->
+  is_false v1 (typeof a1) ->
+  Csem.eval_expr ge e m a3 v3 ->
+  eval_expr_prop a3 v3 ->
+  eval_expr_prop (Expr (Csyntax.Econdition a1 a2 a3) ty) v3.
+Proof.
+  intros; red; intros. inv WT. monadInv TR. 
+  exploit make_boolean_correct_false. eapply H0; eauto. eauto.
+  intros [vb [EVAL ISTRUE]].
+  eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto.
+  simpl. eauto. 
+Qed.
+
 Lemma transl_Eorbool_1_correct:
   forall (a1 a2 : Csyntax.expr) (ty : type) (v1 : val),
   Csem.eval_expr ge e m a1 v1 ->
@@ -681,20 +713,6 @@ Proof.
   eauto.
 Qed.
 
-Lemma transl_Eindex_correct:
-  forall (a1 a2 : Csyntax.expr) (ty : type) (v1 v2 : val) (l : block)
-         (ofs : int),
-  Csem.eval_expr ge e m a1 v1 ->
-  eval_expr_prop a1 v1 ->
-  Csem.eval_expr ge e m a2 v2 ->
-  eval_expr_prop a2 v2 ->
-  sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) ->
-  eval_lvalue_prop (Expr (Eindex a1 a2) ty) l ofs.
-Proof.
-  intros; red; intros. inversion WT; clear WT; subst. simpl in TR. monadInv TR.
-  eapply (make_add_correct tprog); eauto. 
-Qed.
-
 Lemma transl_Efield_struct_correct:
   forall (a : Csyntax.expr) (i : ident) (ty : type) (l : block)
          (ofs : int) (id : ident) (fList : fieldlist) (delta : Z),
@@ -736,6 +754,8 @@ Proof
          transl_Esizeof_correct
          transl_Eunop_correct
          transl_Ebinop_correct
+         transl_Econdition_true_correct
+         transl_Econdition_false_correct
          transl_Eorbool_1_correct
          transl_Eorbool_2_correct
          transl_Eandbool_1_correct
@@ -744,7 +764,6 @@ Proof
          transl_Evar_local_correct
          transl_Evar_global_correct
          transl_Ederef_correct
-         transl_Eindex_correct
          transl_Efield_struct_correct
          transl_Efield_union_correct).
 
@@ -761,6 +780,8 @@ Proof
          transl_Esizeof_correct
          transl_Eunop_correct
          transl_Ebinop_correct
+         transl_Econdition_true_correct
+         transl_Econdition_false_correct
          transl_Eorbool_1_correct
          transl_Eorbool_2_correct
          transl_Eandbool_1_correct
@@ -769,7 +790,6 @@ Proof
          transl_Evar_local_correct
          transl_Evar_global_correct
          transl_Ederef_correct
-         transl_Eindex_correct
          transl_Efield_struct_correct
          transl_Efield_union_correct).