diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2021-06-18 18:35:50 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2021-06-18 18:35:50 +0200 |
| commit | 5798f56b8a8630e43dbed84a824811a5626a1503 (patch) | |
| tree | bee034c6b707a83a4e3e969650c2e2fc6ccb6358 /backend/CSEproof.v | |
| parent | 04b2489d7c2a9b0d203b3d431517367a07bd6b30 (diff) | |
| download | compcert-kvx-5798f56b8a8630e43dbed84a824811a5626a1503.tar.gz compcert-kvx-5798f56b8a8630e43dbed84a824811a5626a1503.zip | |
Replacing default notrap load value by Vundef everywherecsix-PhD
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 5 |
1 files changed, 2 insertions, 3 deletions
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. } { |