From 8f972659841ad38f6f548161b5ca3cfcbdd135cb Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 13 Mar 2019 10:53:15 +0100 Subject: Enlevé la dépendance mémoire de Pcbu MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/Asmblockgenproof1.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 1a55f58e..5486a497 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -743,7 +743,7 @@ Lemma transl_opt_compuimm_correct: exists rs', exists insn, exec_straight_opt (transl_opt_compuimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) - /\ ( Val.cmpu_bool (Mem.valid_pointer m) cmp rs#r1 (Vint n) = Some b -> + /\ ( Val_cmpu_bool cmp rs#r1 (Vint n) = Some b -> exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b)) . Proof. @@ -819,7 +819,7 @@ Lemma transl_opt_compluimm_correct: exists rs', exists insn, exec_straight_opt (transl_opt_compluimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) - /\ ( Val.cmplu_bool (Mem.valid_pointer m) cmp rs#r1 (Vlong n) = Some b -> + /\ ( Val_cmplu_bool cmp rs#r1 (Vlong n) = Some b -> exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b)) . Proof. @@ -1016,7 +1016,7 @@ Proof. exists rs', i. split. * apply A. - * split; auto. apply C. apply EVAL'. + * split; eauto. (* apply C. apply EVAL'. *) + assert (transl_opt_compluimm n c0 x lbl k = loadimm64 RTMP n ::g transl_compl c0 Unsigned x RTMP lbl k). { unfold transl_opt_compluimm. destruct (Int64.eq n Int64.zero) eqn:EQN. -- cgit