From a74f6b45d72834b5b8417297017bd81424123d98 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 7 Mar 2010 15:52:58 +0000 Subject: 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 --- driver/Complements.v | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) (limited to 'driver') 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: -- cgit v1.2.3