diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-09 18:06:30 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-17 17:14:48 +0200 |
| commit | 139595171a98e6722503202a2a8fb7c000f267c2 (patch) | |
| tree | 0946906744fa10aca528251860338be388dff8fb /mppa_k1c/Asmgenproof.v | |
| parent | b63085295d8495ff640f5eaff8b8ad52fc5c43d1 (diff) | |
| download | compcert-kvx-139595171a98e6722503202a2a8fb7c000f267c2.tar.gz compcert-kvx-139595171a98e6722503202a2a8fb7c000f267c2.zip | |
MPPA - added Oaddrstack - problem in TargetPrinter.ml Pbuiltin EF_annot
Conflicts:
mppa_k1c/Asmgenproof1.v
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 60616311..4150cba8 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -159,15 +159,15 @@ Proof. (*unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.*) Qed. Hint Resolve opimm64_label: labels. -(* + Remark addptrofs_label: forall r1 r2 n k, tail_nolabel k (addptrofs r1 r2 n k). Proof. unfold addptrofs; intros. destruct (Ptrofs.eq_dec n Ptrofs.zero). TailNoLabel. - destruct Archi.ptr64. apply opimm64_label; TailNoLabel. apply opimm32_label; TailNoLabel. + apply opimm64_label; TailNoLabel. Qed. Hint Resolve addptrofs_label: labels. - +(* Remark transl_cond_float_nolabel: forall c r1 r2 r3 insn normal, transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn. |