From 5798f56b8a8630e43dbed84a824811a5626a1503 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Fri, 18 Jun 2021 18:35:50 +0200
Subject: Replacing default notrap load value by Vundef everywhere

---
 backend/RTLtyping.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backend/RTLtyping.v')

diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 15ed6d8a..6048f895 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -858,7 +858,7 @@ Lemma wt_exec_Iload_notrap:
   forall env f chunk addr args dst s rs,
   wt_instr f env (Iload NOTRAP chunk addr args dst s) ->
   wt_regset env rs ->
-  wt_regset env (rs#dst <- (default_notrap_load_value chunk)).
+  wt_regset env (rs#dst <- Vundef).
 Proof.
   intros. 
   eapply wt_regset_assign; eauto. simpl. trivial.
-- 
cgit