From b063fb03af84483671833d40491f4fa8d2c8b4c9 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 23 Jul 2021 18:25:00 +0200 Subject: non trapping loads --- scheduling/BTLtoRTLproof.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'scheduling/BTLtoRTLproof.v') diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 9b8dabab..324f1d14 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -230,7 +230,8 @@ Proof. intros; rewrite symbols_preserved; trivial. - (* exec_load *) inv MIB. exists pc'; split; auto; constructor. - apply plus_one. eapply exec_Iload; eauto. + apply plus_one. inv LOAD. + eapply exec_Iload; eauto. all: erewrite <- eval_addressing_preserved; eauto; intros; rewrite symbols_preserved; trivial. - (* exec_store *) -- cgit