From 906a8553570ed17a8e90831c1d1df18d76e94154 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 6 May 2019 13:51:51 +0200 Subject: simplification semantique+preuve des load_q+load_o --- mppa_k1c/lib/Asmblockgenproof0.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'mppa_k1c/lib') diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index e8835a82..a8da1cf1 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -953,19 +953,17 @@ Proof. - (* PLoadQRRO *) unfold parexec_load_q_offset in H1. destruct (gpreg_q_expand _) as [r0 r1] in H1. - destruct (ireg_eq _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. + inv H1. Simpl. - (* PLoadORRO *) unfold parexec_load_o_offset in H1. destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. - destruct (orb _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. + inv H1. Simpl. - (* PStoreQRRO *) unfold parexec_store_q_offset in H1. destruct (gpreg_q_expand _) as [r0 r1] in H1. -- cgit