From 5798f56b8a8630e43dbed84a824811a5626a1503 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 18 Jun 2021 18:35:50 +0200 Subject: Replacing default notrap load value by Vundef everywhere --- kvx/Asmblockprops.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kvx/Asmblockprops.v') 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. -- cgit