diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-08-30 16:11:18 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:58:31 +0200 |
| commit | bcc47e526b2b6e5fd3c8e2b68cadb70628075ea0 (patch) | |
| tree | e29a3bf1fc440ddf82c85bb4bd1f1273173f101d /mppa_k1c/Asmblock.v | |
| parent | 63737a502b0f0b6c1369641e9d3d9f05712e74f7 (diff) | |
| download | compcert-kvx-bcc47e526b2b6e5fd3c8e2b68cadb70628075ea0.tar.gz compcert-kvx-bcc47e526b2b6e5fd3c8e2b68cadb70628075ea0.zip | |
Example of Program use...
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index c83867f1..4d7ff03c 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -510,6 +510,20 @@ Qed. (** * Utility for Asmblockgen *) +Program Definition bblock_single_inst (i: instruction) := + match i with + | PBasic b => {| header:=nil; body:=(b::nil); exit:=None |} + | PControl ctl => {| header:=nil; body:=nil; exit:=(Some ctl) |} + end. +Obligation 1. + intros. split. left; discriminate. discriminate. +Qed. +Obligation 2. + intros. split. right; discriminate. + unfold builtin_alone. intros. auto. +Qed. + +(* Example bblock_single_basic_correct : forall i, wf_bblock nil (i::nil) None. Proof. intros. split. left; discriminate. discriminate. @@ -521,6 +535,7 @@ Proof. unfold builtin_alone. intros. auto. Qed. + Definition bblock_single_inst (i: instruction) := match i with | PBasic b => {| header:=nil; body:=(b::nil); exit:=None; @@ -528,6 +543,7 @@ Definition bblock_single_inst (i: instruction) := | PControl ctl => {| header:=nil; body:=nil; exit:=(Some ctl); correct:=bblock_single_control_correct ctl |} end. +*) (** * Operational semantics *) |