diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-01 21:54:11 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-01 21:54:11 +0200 |
| commit | cbe3f094b32077ce8d8569556d4ebc6341b09dd9 (patch) | |
| tree | 61824ef04196070b165e18f788b7cca153087bc0 /mppa_k1c/lib | |
| parent | 98be0205d9d29378fb272a9f424144651bd8afec (diff) | |
| download | compcert-kvx-cbe3f094b32077ce8d8569556d4ebc6341b09dd9.tar.gz compcert-kvx-cbe3f094b32077ce8d8569556d4ebc6341b09dd9.zip | |
it compiles
Diffstat (limited to 'mppa_k1c/lib')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index ab0d2964..0a83a903 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -949,6 +949,7 @@ Proof. 1-10: try (unfold parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). 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. - 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. |