diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-10 17:22:34 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-10 17:22:34 +0200 |
| commit | 8bdfa912a9ba8cee569cb40bf2ec4c584095e402 (patch) | |
| tree | 3e6711d7bcf5ee1d92241d4141f7bbd37e4dcaf4 /mppa_k1c/Asmgenproof1.v | |
| parent | 67a5ffd5f8a1f2f95dc480daee9b5d927c768a2d (diff) | |
| download | compcert-kvx-8bdfa912a9ba8cee569cb40bf2ec4c584095e402.tar.gz compcert-kvx-8bdfa912a9ba8cee569cb40bf2ec4c584095e402.zip | |
MPPA - Added Mload
Diffstat (limited to 'mppa_k1c/Asmgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof1.v | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index aeee5e9e..55724239 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -1431,16 +1431,27 @@ Lemma transl_memory_access_correct: Proof. intros until v; intros TR EV. unfold transl_memory_access in TR; destruct addr; ArgsInv. -(* - (* indexed *) inv EV. apply indexed_memory_access_correct; eauto with asmgen. - (* global *) simpl in EV. inv EV. inv TR. econstructor; econstructor; econstructor; split. constructor. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. unfold eval_offset. apply low_high_half. + split; intros; Simpl. unfold eval_offset. + assert (Val.lessdef (Val.offset_ptr (Genv.symbol_address ge i i0) Ptrofs.zero) (Genv.symbol_address ge i i0)). + { apply Val.offset_ptr_zero. } + remember (Genv.symbol_address ge i i0) as symbol. + destruct symbol; auto. + + contradict Heqsymbol; unfold Genv.symbol_address; + destruct (Genv.find_symbol ge i); discriminate. + + contradict Heqsymbol; unfold Genv.symbol_address; + destruct (Genv.find_symbol ge i); discriminate. + + contradict Heqsymbol; unfold Genv.symbol_address; + destruct (Genv.find_symbol ge i); discriminate. + + contradict Heqsymbol; unfold Genv.symbol_address; + destruct (Genv.find_symbol ge i); discriminate. + + simpl. rewrite Ptrofs.add_zero; auto. - (* stack *) inv TR. inv EV. apply indexed_memory_access_correct; eauto with asmgen. -*) Qed. Lemma transl_load_access_correct: |