diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-06 13:51:51 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-06 13:51:51 +0200 |
| commit | 906a8553570ed17a8e90831c1d1df18d76e94154 (patch) | |
| tree | b8a1ecf6d8fe96aa4ece54424177cc4662950b82 /mppa_k1c/lib | |
| parent | 20fed399133f75a10599082c9f75d9a519efff52 (diff) | |
| download | compcert-kvx-906a8553570ed17a8e90831c1d1df18d76e94154.tar.gz compcert-kvx-906a8553570ed17a8e90831c1d1df18d76e94154.zip | |
simplification semantique+preuve des load_q+load_o
Diffstat (limited to 'mppa_k1c/lib')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 6 |
1 files changed, 2 insertions, 4 deletions
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. |