From 5530915001c3e8b395d731480e5a6618a08af7af Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Nov 2021 10:57:22 +0100 Subject: being more archi-independant --- backend/RTLTunnelingproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/RTLTunnelingproof.v') diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index 2cef08e2..aa21fc06 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -461,7 +461,7 @@ Proof. left. eexists. split. * eapply exec_Iload. -- exploit instruction_type_preserved; (simpl; eauto)||congruence. - -- eapply has_loaded_normal; eauto. rewrite <- EVAL'. apply eval_addressing_preserved. apply symbols_preserved. + -- try (eapply has_loaded_normal; eauto; rewrite <- EVAL'; apply eval_addressing_preserved; apply symbols_preserved). * apply match_states_intro; try assumption. apply set_reg_lessdef. apply LD'. apply RS. + destruct (eval_addressing) eqn:EVAL in LOAD. * specialize (LOAD v). @@ -473,7 +473,7 @@ Proof. -- left; eexists; split. eapply exec_Iload. ++ exploit instruction_type_preserved; (simpl; eauto)||congruence. - ++ eapply has_loaded_normal; eauto. rewrite <- ADDR. apply eval_addressing_preserved. apply symbols_preserved. + ++ try (eapply has_loaded_normal; eauto; rewrite <- ADDR; apply eval_addressing_preserved; apply symbols_preserved). ++ apply match_states_intro; try assumption. apply set_reg_lessdef; eauto. -- left; eexists; split. eapply exec_Iload. -- cgit