diff options
Diffstat (limited to 'backend/Linear.v')
| -rw-r--r-- | backend/Linear.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Linear.v b/backend/Linear.v index 1443f795..cb11f7dc 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -170,7 +170,7 @@ Inductive step: state -> trace -> state -> Prop := forall s f sp chunk addr args dst b rs m rs', eval_addressing ge sp addr (reglist rs args) = None -> rs' = Locmap.set (R dst) - (default_notrap_load_value chunk) + Vundef (undef_regs (destroyed_by_load chunk addr) rs) -> step (State s f sp (Lload NOTRAP chunk addr args dst :: b) rs m) E0 (State s f sp b rs' m) @@ -179,7 +179,7 @@ Inductive step: state -> trace -> state -> Prop := eval_addressing ge sp addr (reglist rs args) = Some a -> Mem.loadv chunk m a = None -> rs' = Locmap.set (R dst) - (default_notrap_load_value chunk) + Vundef (undef_regs (destroyed_by_load chunk addr) rs) -> step (State s f sp (Lload NOTRAP chunk addr args dst :: b) rs m) E0 (State s f sp b rs' m) |