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 /kvx/Asmblockprops.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 'kvx/Asmblockprops.v')
| -rw-r--r-- | kvx/Asmblockprops.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kvx/Asmblockprops.v b/kvx/Asmblockprops.v index c3929be5..a732d29b 100644 --- a/kvx/Asmblockprops.v +++ b/kvx/Asmblockprops.v @@ -96,9 +96,9 @@ Theorem exec_basic_instr_pc: Proof. intros. destruct b; try destruct i; try destruct i. all: try (inv H; Simpl). - 1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail. + 1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; inv H1; Simpl; fail. - 1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail. + 1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; inv H1; Simpl; fail. { (* PLoadQRRO *) unfold parexec_load_q_offset in H1. |