diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-13 10:53:15 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-13 10:53:15 +0100 |
| commit | 8f972659841ad38f6f548161b5ca3cfcbdd135cb (patch) | |
| tree | ef33c46495536c075ae940d9e08cf89302eaf83e /mppa_k1c/Asmblockgenproof1.v | |
| parent | 605f0a1b6a6d4e5e9ada867baebc3e56736fe920 (diff) | |
| download | compcert-kvx-8f972659841ad38f6f548161b5ca3cfcbdd135cb.tar.gz compcert-kvx-8f972659841ad38f6f548161b5ca3cfcbdd135cb.zip | |
Enlevé la dépendance mémoire de Pcbu
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |