Replacing default notrap load value by Vundef everywherecsix-PhD

3 files changed, 5 insertions, 5 deletions

diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v
index a4fce97e..b29a7759 100644
--- a/scheduling/RTLpath.v
+++ b/scheduling/RTLpath.v
@@ -156,7 +156,7 @@ Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem)
       SOME v <- Mem.loadv chunk m a IN
       Some (mk_istate true pc' (rs#dst <- v) m)
   | Iload NOTRAP chunk addr args dst pc' =>
-      let default_state := mk_istate true pc' rs#dst <- (default_notrap_load_value chunk) m in
+      let default_state := mk_istate true pc' rs#dst <- Vundef m in
       match (eval_addressing ge sp addr rs##args) with
       | None => Some default_state
       | Some a => match (Mem.loadv chunk m a) with
diff --git a/scheduling/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v
index aa8db342..2a791feb 100644
--- a/scheduling/RTLpathSE_theory.v
+++ b/scheduling/RTLpathSE_theory.v
@@ -87,11 +87,11 @@ Fixpoint seval_sval (ge: RTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem):
       | NOTRAP =>
           SOME args <- seval_list_sval ge sp lsv rs0 m0 IN
           match (eval_addressing ge sp addr args) with
-          | None => Some (default_notrap_load_value chunk)
+          | None => Some Vundef
           | Some a =>
               SOME m <- seval_smem ge sp sm rs0 m0 IN
               match (Mem.loadv chunk m a) with
-              | None => Some (default_notrap_load_value chunk)
+              | None => Some Vundef
               | Some val => Some val
               end
           end
diff --git a/scheduling/postpass_lib/Machblock.v b/scheduling/postpass_lib/Machblock.v
index c8eadbd7..b588cca8 100644
--- a/scheduling/postpass_lib/Machblock.v
+++ b/scheduling/postpass_lib/Machblock.v
@@ -237,13 +237,13 @@ Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (m:
   | exec_MBload_notrap1:
       forall addr args rs' chunk dst,
       eval_addressing ge sp addr rs##args = None ->
-      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) ->
+      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- Vundef) ->
       basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m
   | exec_MBload_notrap2:
       forall addr args a rs' chunk dst,
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.loadv chunk m a = None ->
-      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) ->
+      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- Vundef) ->
       basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m
   | exec_MBstore:
       forall chunk addr args src m' a rs',