diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 15:26:03 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 15:26:03 +0200 |
| commit | a6c79438ae754d969558bd37eb3a7676be6e66aa (patch) | |
| tree | 18f70fc6ef416e53638c445fa8ca745aef0b0fe1 /mppa_k1c/Asmgenproof.v | |
| parent | 5e35117f8dd7cc4c548ecd704e11f3ca8845dedd (diff) | |
| download | compcert-kvx-a6c79438ae754d969558bd37eb3a7676be6e66aa.tar.gz compcert-kvx-a6c79438ae754d969558bd37eb3a7676be6e66aa.zip | |
MPPA - Ocast32signed
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 4809afcb..905bb85c 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -142,6 +142,13 @@ Proof. Qed. Hint Resolve loadimm64_label: labels. +Remark cast32signed_label: + forall rd rs k, tail_nolabel k (cast32signed rd rs k). +Proof. + intros; unfold cast32signed. destruct (ireg_eq rd rs); TailNoLabel. +Qed. +Hint Resolve cast32signed_label: labels. + Remark opimm64_label: forall op opimm r1 r2 n k, (forall r1 r2 r3, nolabel (op r1 r2 r3)) -> |