diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-19 11:42:30 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:08 +0200 |
| commit | 1c1dd8c9cfcc98f183f6844b6c2f4ae60edd165d (patch) | |
| tree | fa2c37098369a22ec7e6150ea7e4ed5fd4e529d3 /mppa_k1c/Asmgenproof.v | |
| parent | 734ef70ef9edcd69d822d573628d5f0ca282ddcb (diff) | |
| download | compcert-kvx-1c1dd8c9cfcc98f183f6844b6c2f4ae60edd165d.tar.gz compcert-kvx-1c1dd8c9cfcc98f183f6844b6c2f4ae60edd165d.zip | |
MPPA - Activated Paddw and Paddiw + ops
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 45531e00..414527ad 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -122,7 +122,7 @@ Proof. (*unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.*) Qed. Hint Resolve loadimm32_label: labels. -(* + Remark opimm32_label: forall op opimm r1 r2 n k, (forall r1 r2 r3, nolabel (op r1 r2 r3)) -> @@ -130,10 +130,10 @@ Remark opimm32_label: tail_nolabel k (opimm32 op opimm r1 r2 n k). Proof. intros; unfold opimm32. destruct (make_immed32 n); TailNoLabel. - unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel. +(*unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.*) Qed. Hint Resolve opimm32_label: labels. -*) + Remark loadimm64_label: forall r n k, tail_nolabel k (loadimm64 r n k). Proof. @@ -277,6 +277,7 @@ Remark transl_op_label: Proof. Opaque Int.eq. unfold transl_op; intros; destruct op; TailNoLabel. +- apply opimm32_label; intros; exact I. - apply opimm64_label; intros; exact I. Qed. |