Merge of the "princeton" branch:

- Define type "block" as "positive" instead of "Z".
- Strengthen mem_unchanged_on so that the permissions are identical,
  instead of possibly increasing.
- Move mem_unchanged_on from Events to Memory.Mem.
- Define it in terms of mem_contents rather than in terms of Mem.load.
- ExportClight: try to name temporaries introduced by SimplExpr
- SimplExpr: avoid reusing temporaries between different functions,
  instead, thread a single generator through all functions.


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

4 files changed, 5 insertions, 5 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 0609ac0..24dedc7 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -797,7 +797,7 @@ Inductive initial_state (p: program): state -> Prop :=
         (Pregmap.init Vundef)
         # PC <- (symbol_offset ge p.(prog_main) Int.zero)
         # RA <- Vzero
-        # ESP <- (Vptr Mem.nullptr Int.zero) in
+        # ESP <- Vzero in
       initial_state p (State rs0 m0).
 
 Inductive final_state: state -> int -> Prop :=
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index f6eefbd..df09ca7 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -905,7 +905,7 @@ Proof.
   econstructor; eauto.
   constructor.
   apply Mem.extends_refl.
-  split. auto. simpl. congruence. intros. rewrite Regmap.gi. auto. 
+  split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. 
   unfold symbol_offset. 
   rewrite (transform_partial_program_main _ _ TRANSF).
   rewrite symbols_preserved. 
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 00b706c..0bf030c 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -550,7 +550,7 @@ Proof.
   simpl. 
   fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *.
   fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *.
-  destruct (zeq b0 b1).
+  destruct (eq_block b0 b1).
   destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i) &&
             Mem.weak_valid_pointer m b1 (Int.unsigned i0)); inversion H1.
   destruct c; simpl; auto.
diff --git a/ia32/Op.v b/ia32/Op.v
index 4ac961b..509938e 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -384,7 +384,7 @@ Proof with (try exact I).
   destruct v0...
   destruct v0...
   destruct v0...
-  destruct v0; destruct v1... simpl. destruct (zeq b b0)...
+  destruct v0; destruct v1... simpl. destruct (eq_block b b0)...
   destruct v0; destruct v1...
   destruct v0...
   destruct v0; destruct v1; simpl in *; inv H0.
@@ -792,7 +792,7 @@ Proof.
   inv H4; simpl; auto.
   inv H4; inv H2; simpl; auto. econstructor; eauto. 
     rewrite Int.sub_add_l. auto.
-    destruct (zeq b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite zeq_true. 
+    destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. 
     rewrite Int.sub_shifted. auto.
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.