Merge of the newmem and newextcalls branches:

- Revised memory model with concrete representation of ints & floats,
  and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.


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

1 files changed, 7 insertions, 9 deletions

diff --git a/driver/Complements.v b/driver/Complements.v
index 6fe5038..b76a99f 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -51,31 +51,29 @@ Qed.
 
 Lemma step_internal_deterministic:
   forall ge s t1 s1 t2 s2,
-  Asm.step ge s t1 s1 -> Asm.step ge s t2 s2 -> internal_determinism _ t1 s1 t2 s2.
+  Asm.step ge s t1 s1 -> Asm.step ge s t2 s2 -> matching_traces t1 t2 ->
+  s1 = s2 /\ t1 = t2.
 Proof.
   intros. inv H; inv H0.
   assert (c0 = c) by congruence.
   assert (i0 = i) by congruence.
   assert (rs'0 = rs') by congruence.
   assert (m'0 = m') by congruence.
-  subst. constructor.
+  subst. auto. 
   congruence.
   congruence.
   assert (ef0 = ef) by congruence. subst ef0.
   assert (args0 = args). eapply extcall_arguments_deterministic; eauto. subst args0.
-  inv H3; inv H8.
-  assert (eargs0 = eargs). eapply eventval_list_match_deterministic; eauto. subst eargs0.
-  constructor. intros.
-  exploit eventval_match_deterministic. eexact H0. eexact H5. intros. 
-  assert (res = res0). tauto. 
-  congruence.
+  exploit external_call_determ. eexact H4. eexact H9. auto. 
+  intros [A [B C]]. subst. 
+  intuition congruence.
 Qed.
 
 Lemma initial_state_deterministic:
   forall p s1 s2,
   initial_state p s1 -> initial_state p s2 -> s1 = s2.
 Proof.
-  intros. inv H; inv H0. reflexivity. 
+  intros. inv H; inv H0. f_equal. congruence.
 Qed.
 
 Lemma final_state_not_step: