diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 03:33:58 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 03:33:58 +0200 |
| commit | 8163278174362fb8269804a7958f6e9e7878a511 (patch) | |
| tree | 443fe57bfde8cacb7806c3a8dd69f499709bdee4 /mppa_k1c/lib | |
| parent | 5d09dd8f3194ecc90137178d6b5d18b9ad31aabf (diff) | |
| download | compcert-kvx-8163278174362fb8269804a7958f6e9e7878a511.tar.gz compcert-kvx-8163278174362fb8269804a7958f6e9e7878a511.zip | |
getting stuck need to move offsets
Diffstat (limited to 'mppa_k1c/lib')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 0a83a903..a93cb28a 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -950,6 +950,13 @@ Proof. 1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). 1-10: try (unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. 1-10: try (unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. + - (* PStoreQRRO *) + unfold parexec_store_q_offset in H1. + destruct (gpreg_q_expand _) as [r0 r1] in H1. + destruct (eval_offset _ _) in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + inv H1. Simpl. reflexivity. - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate. destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate. |