diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-14 11:51:48 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:07 +0200 |
| commit | ad9f97729e9c708f8e220e6d93a1cdb442b60273 (patch) | |
| tree | 6439394772b7dd47be0ee0f680101ada3c2215d1 /mppa_k1c/Asmgenproof.v | |
| parent | 79597131ae07f1fe63485270486755481549470f (diff) | |
| download | compcert-kvx-ad9f97729e9c708f8e220e6d93a1cdb442b60273.tar.gz compcert-kvx-ad9f97729e9c708f8e220e6d93a1cdb442b60273.zip | |
MPPA - Removed Plui, replaced with Pmake, and modified make_immed64
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 51d093f8..568311f5 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -149,7 +149,7 @@ Remark opimm64_label: tail_nolabel k (opimm64 op opimm r1 r2 n k). Proof. intros; unfold opimm64. destruct (make_immed64 n); TailNoLabel. - unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel. +(*unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.*) Qed. Hint Resolve opimm64_label: labels. (* @@ -414,7 +414,8 @@ Lemma transl_find_label: Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ. rewrite transl_code'_transl_code in EQ0. unfold fn_code. - simpl. destruct (storeind_ptr_label GPR8 GPR12 (fn_retaddr_ofs f) x) as [A B]; rewrite B. + simpl. destruct (storeind_ptr_label GPR8 GPR12 (fn_retaddr_ofs f) x) as [A B]. + (* destruct B. *) eapply transl_code_label; eauto. Qed. |