From 5798f56b8a8630e43dbed84a824811a5626a1503 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 18 Jun 2021 18:35:50 +0200 Subject: Replacing default notrap load value by Vundef everywhere --- backend/CSEproof.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'backend/CSEproof.v') diff --git a/backend/CSEproof.v b/backend/CSEproof.v index cf51f5a2..556b44b3 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -402,7 +402,7 @@ Lemma add_load_holds_none1: forall valu1 ge sp rs m n addr (args: list reg) chunk dst, numbering_holds valu1 ge sp rs m n -> eval_addressing ge sp addr rs##args = None -> - exists valu2, numbering_holds valu2 ge sp (rs#dst <- (default_notrap_load_value chunk)) m (add_load n dst chunk addr args). + exists valu2, numbering_holds valu2 ge sp (rs#dst <- Vundef) m (add_load n dst chunk addr args). Proof. unfold add_load; intros. destruct (valnum_regs n args) as [n1 vl] eqn:VN. @@ -418,7 +418,7 @@ Lemma add_load_holds_none2: numbering_holds valu1 ge sp rs m n -> eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = None -> - exists valu2, numbering_holds valu2 ge sp (rs#dst <- (default_notrap_load_value chunk)) m (add_load n dst NOTRAP chunk addr args). + exists valu2, numbering_holds valu2 ge sp (rs#dst <- Vundef) m (add_load n dst NOTRAP chunk addr args). Proof. unfold add_load; intros. destruct (valnum_regs n args) as [n1 vl] eqn:VN. @@ -1210,7 +1210,6 @@ Proof. exists valu1. apply set_unknown_holds. assumption. - unfold default_notrap_load_value. apply set_reg_lessdef; eauto. } { -- cgit