diff options
Diffstat (limited to 'riscV/Asmgenproof.v')
| -rw-r--r-- | riscV/Asmgenproof.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 63287a50..8e9f022c 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -359,7 +359,7 @@ Proof. - destruct ep. eapply loadind_label; eauto. eapply tail_nolabel_trans. apply loadind_ptr_label. eapply loadind_label; eauto. - eapply transl_op_label; eauto. -- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. +- destruct t; (try discriminate); destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. - destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. - destruct s0; monadInv H; TailNoLabel. - destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]). @@ -725,6 +725,12 @@ Local Transparent destroyed_by_op. intros; auto with asmgen. simpl; congruence. +- (* Mload notrap *) (* isn't there a nicer way? *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + +- (* Mload notrap *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + - (* Mstore *) assert (eval_addressing tge sp addr (map rs args) = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. |