- Added alignment constraints to memory loads and stores.

- In Cminor and below, removed pointer validity check in semantics of 
  comparisons, so that evaluation of expressions is independent of
  memory state.
- In Cminor and below, removed "alloc" instruction.
- Cleaned up commented-away parts.


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

1 files changed, 2 insertions, 18 deletions

diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 1074dddb..6d5cd8ea 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -568,7 +568,7 @@ Lemma transl_expr_Eop_correct:
          (vargs : list val) (v : val),
   eval_exprlist ge sp e m le args vargs ->
   transl_exprlist_prop le args vargs ->
-  eval_operation ge sp op vargs m = Some v ->
+  eval_operation ge sp op vargs = Some v ->
   transl_expr_prop le (Eop op args) v.
 Proof.
   intros; red; intros. inv TE. 
@@ -711,7 +711,7 @@ Lemma transl_condition_CEcond_correct:
          (vargs : list val) (b : bool),
   eval_exprlist ge sp e m le args vargs ->
   transl_exprlist_prop le args vargs ->
-  eval_condition cond vargs m = Some b ->
+  eval_condition cond vargs = Some b ->
   transl_condition_prop le (CEcond cond args) b.
 Proof.
   intros; red; intros; inv TE.
@@ -1154,22 +1154,6 @@ Proof.
   apply sig_transl_function; auto.
   traceEq.
   rewrite G. constructor; auto.
-
-  (* alloc *)
-  inv TS. 
-  exploit transl_expr_correct; eauto. 
-  intros [rs1 [A [B [C D]]]].
-  set (rs2 := rs1#rd <- (Vptr b Int.zero)).
-  assert (match_env map e nil rs2). unfold rs2; eauto with rtlg. 
-  exploit tr_store_var_correct. eauto. auto. eexact H1. 
-  intros [rs3 [E F]].
-  unfold rs2 in F. rewrite Regmap.gss in F.
-  econstructor; split.
-  left. apply plus_star_trans with E0 (State cs c sp n2 rs2 m') E0.
-  eapply plus_right. eexact A. unfold rs2. eapply exec_Ialloc; eauto. traceEq.
-  eexact E. traceEq.
-  econstructor; eauto. constructor.
-
   (* seq *)
   inv TS. 
   econstructor; split.