diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-07 16:26:28 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-07 16:26:28 +0100 |
| commit | d4e023d87ec851ca3b670b45327c95600f4afee4 (patch) | |
| tree | b12601648bd6e0dd5262866ca1d5935f23870294 /mppa_k1c/Asmblockgenproof.v | |
| parent | b976979ce673c693dec0fc9c28c43d5b63ebd9b1 (diff) | |
| download | compcert-kvx-d4e023d87ec851ca3b670b45327c95600f4afee4.tar.gz compcert-kvx-d4e023d87ec851ca3b670b45327c95600f4afee4.zip | |
Fix minor proof
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 1ac9a211..84877488 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -891,6 +891,10 @@ Proof. + simpl in TIC. unfold transl_cbranch in TIC. exploreInst; simpl; eauto.
* unfold transl_opt_compuimm. exploreInst; simpl; eauto.
* unfold transl_opt_compluimm. exploreInst; simpl; eauto.
+ * unfold transl_comp_float64. exploreInst; simpl; eauto.
+ * unfold transl_comp_notfloat64. exploreInst; simpl; eauto.
+ * unfold transl_comp_float32. exploreInst; simpl; eauto.
+ * unfold transl_comp_notfloat32. exploreInst; simpl; eauto.
+ simpl in TIC. inv TIC.
+ simpl in TIC. monadInv TIC. simpl. eauto.
- monadInv TIC. simpl; auto.
@@ -990,6 +994,10 @@ Proof. + simpl in TIC. unfold transl_cbranch in TIC. exploreInst; try discriminate.
* unfold transl_opt_compuimm. exploreInst; try discriminate.
* unfold transl_opt_compluimm. exploreInst; try discriminate.
+ * unfold transl_comp_float64. exploreInst; try discriminate.
+ * unfold transl_comp_notfloat64. exploreInst; try discriminate.
+ * unfold transl_comp_float32. exploreInst; try discriminate.
+ * unfold transl_comp_notfloat32. exploreInst; try discriminate.
- contradict Hnonil; auto.
Qed.
@@ -1005,8 +1013,12 @@ Proof. - assert False. eapply Hnobuiltin; eauto. destruct H.
- unfold transl_cbranch in TIC. exploreInst.
all: try discriminate.
- + unfold transl_opt_compuimm. exploreInst. all: try discriminate.
- + unfold transl_opt_compluimm. exploreInst. all: try discriminate.
+ * unfold transl_opt_compuimm. exploreInst. all: try discriminate.
+ * unfold transl_opt_compluimm. exploreInst. all: try discriminate.
+ * unfold transl_comp_float64. exploreInst; try discriminate.
+ * unfold transl_comp_notfloat64. exploreInst; try discriminate.
+ * unfold transl_comp_float32. exploreInst; try discriminate.
+ * unfold transl_comp_notfloat32. exploreInst; try discriminate.
Qed.
Theorem match_state_codestate:
|