diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 16:32:35 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 16:32:35 +0200 |
| commit | 919d1dfbf22967ae9686d5b982b51cfa707b5edd (patch) | |
| tree | a16e3dc736f47cbf272f0e821909db04d42cfd69 /mppa_k1c/lib/Asmblockgenproof0.v | |
| parent | d9ac009e14007e7b7e45e82f6187ae31d14aee94 (diff) | |
| download | compcert-kvx-919d1dfbf22967ae9686d5b982b51cfa707b5edd.tar.gz compcert-kvx-919d1dfbf22967ae9686d5b982b51cfa707b5edd.zip | |
begin add Plq
Diffstat (limited to 'mppa_k1c/lib/Asmblockgenproof0.v')
| -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 3bca6629..9303b780 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 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. + - (* 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. - (* PStoreQRRO *) unfold parexec_store_q_offset in H1. destruct (gpreg_q_expand _) as [r0 r1] in H1. |