From 1fbe45e2d1f02ef6e8fb6fe7545728a744e047b8 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sat, 24 Jul 2021 11:49:14 +0200 Subject: remove default_notrap_load_value --- backend/RTLTunnelingproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend') diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index 14a2c037..51ef0f7a 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -531,7 +531,7 @@ Proof. + eapply exec_Iload_notrap1. * exploit instruction_type_preserved; (simpl; eauto)||congruence. * rewrite <- H1. apply eval_addressing_preserved. apply symbols_preserved. - + apply match_states_intro; try assumption. apply set_reg_lessdef. unfold default_notrap_load_value. apply Val.lessdef_undef. apply RS. + + apply match_states_intro; try assumption. apply set_reg_lessdef. apply Val.lessdef_undef. apply RS. - (* Iload NOTRAP2 *) exploit eval_addressing_lessdef; try eassumption. apply reglist_lessdef; apply RS. -- cgit