diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-04-02 17:37:09 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-04-02 17:37:09 +0200 |
| commit | 4adb0af96c3c0523438e86275f9e23ffdc69e4ba (patch) | |
| tree | b0bef344a09b453b77f2c16a1cd5c32c970d1d8e /mppa_k1c/lib | |
| parent | 0c95673ef97195eae6213db92c2f69ef1d1ff48e (diff) | |
| download | compcert-kvx-4adb0af96c3c0523438e86275f9e23ffdc69e4ba.tar.gz compcert-kvx-4adb0af96c3c0523438e86275f9e23ffdc69e4ba.zip | |
Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yet
Diffstat (limited to 'mppa_k1c/lib')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 69234938..ed8edfde 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -943,14 +943,16 @@ 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 (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 (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. + 1-10: try (unfold exec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; unfold exec_load in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). + 1-10: try (unfold exec_load_reg in H1; destruct (rs1 rofs); try discriminate; unfold exec_load in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). + 1-10: try (unfold exec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; unfold exec_store in H1; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). + 1-10: try (unfold exec_store_reg in H1; destruct (rs1 rofs); try discriminate; unfold exec_store 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. + - destruct rs; try discriminate. inv H1. Simpl. + - destruct rd; try discriminate. inv H1; Simpl. + - reflexivity. Qed. (* Lemma exec_straight_pc': |