diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-02-05 17:34:54 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-02-05 17:34:54 +0100 |
| commit | b7f386c026a573708451ca20b015c021f3f82205 (patch) | |
| tree | c3f11ac22fcce428bc2a22f08dc43395c7e6ca75 /mppa_k1c/lib/Asmblockgenproof0.v | |
| parent | a95feb6be199554760b54186377936d1c1cfb18f (diff) | |
| parent | 2b226da49ea711bfe8139a0fae7c44cb432e2f61 (diff) | |
| download | compcert-kvx-b7f386c026a573708451ca20b015c021f3f82205.tar.gz compcert-kvx-b7f386c026a573708451ca20b015c021f3f82205.zip | |
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
Diffstat (limited to 'mppa_k1c/lib/Asmblockgenproof0.v')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 443e8757..8c299f88 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -937,11 +937,11 @@ Lemma exec_basic_instr_pc: Proof. intros. destruct b; try destruct i; try destruct i. all: try (inv H; Simpl). - all: try (unfold exec_load in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). - all: try (unfold exec_store in H1; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). + all: try (unfold exec_load in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). + all: try (unfold exec_store in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. - destruct (rs1 _); try discriminate. - destruct (Mem.free _ _ _ _). inv H0. Simpl. discriminate. + destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate. + destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate. destruct rs; try discriminate. inv H1. Simpl. destruct rd; try discriminate. inv H1; Simpl. auto. |