diff options
Diffstat (limited to 'backend/Mach.v')
| -rw-r--r-- | backend/Mach.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Mach.v b/backend/Mach.v index 1c6fdb18..2cfd738d 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -330,14 +330,14 @@ Inductive step: state -> trace -> state -> Prop := | exec_Mload_notrap1: forall s f sp chunk addr args dst c rs m rs', 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) -> step (State s f sp (Mload NOTRAP chunk addr args dst :: c) rs m) E0 (State s f sp c rs' m) | exec_Mload_notrap2: forall s f sp chunk addr args dst c rs m a rs', 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) -> step (State s f sp (Mload NOTRAP chunk addr args dst :: c) rs m) E0 (State s f sp c rs' m) | exec_Mstore: |