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/RTL.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/RTL.v')
-rw-r--r-- | backend/RTL.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/RTL.v b/backend/RTL.v index 31b5cf99..fe350adf 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -225,14 +225,14 @@ Inductive step: state -> trace -> state -> Prop := (fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') -> eval_addressing ge sp addr rs##args = None -> step (State s f sp pc rs m) - E0 (State s f sp pc' (rs#dst <- (default_notrap_load_value chunk)) m) + E0 (State s f sp pc' (rs#dst <- Vundef) m) | exec_Iload_notrap2: forall s f sp pc rs m chunk addr args dst pc' a, (fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') -> eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = None-> step (State s f sp pc rs m) - E0 (State s f sp pc' (rs#dst <- (default_notrap_load_value chunk)) m) + E0 (State s f sp pc' (rs#dst <- Vundef) m) | exec_Istore: forall s f sp pc rs m chunk addr args src pc' a m', (fn_code f)!pc = Some(Istore chunk addr args src pc') -> |