diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-22 14:23:35 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-22 14:23:35 +0100 |
| commit | 13effac30e636d890f891863f04c3d379713b34a (patch) | |
| tree | e621161894f58a931abdf4bb3f906cf88e2e2054 /mppa_k1c/Asmblockgenproof.v | |
| parent | 44cfe47f9e5d0c40fad23fccdb4b37b1ea3c1071 (diff) | |
| download | compcert-kvx-13effac30e636d890f891863f04c3d379713b34a.tar.gz compcert-kvx-13effac30e636d890f891863f04c3d379713b34a.zip | |
jumptable avance
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index ea4d1918..f07cb6a4 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -883,11 +883,16 @@ Proof. intros until x2. intros Hbuiltin TIC.
destruct ex.
- destruct c.
+ (* MBcall *)
+ simpl in TIC. exploreInst; simpl; eauto.
+ (* MBtailcall *)
+ simpl in TIC. exploreInst; simpl; eauto.
+ (* MBbuiltin *)
+ assert (H: Some (MBbuiltin e l b) <> Some (MBbuiltin e l b)).
apply Hbuiltin. contradict H; auto.
+ (* MBgoto *)
+ simpl in TIC. exploreInst; simpl; eauto.
+ (* MBcond *)
+ 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.
@@ -895,7 +900,9 @@ Proof. * 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.
+ (* MBjumptable *)
+ + simpl in TIC. exploreInst; simpl; eauto.
+ (* MBreturn *)
+ simpl in TIC. monadInv TIC. simpl. eauto.
- monadInv TIC. simpl; auto.
Qed.
|