diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-02-22 16:57:02 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:06 +0200 |
| commit | f1d3dbb3fa70233d1ad83ae88876dd384346a16a (patch) | |
| tree | 356dd54e5ae0a960eaa60a7b174ceb4fa750f9fc /mppa_k1c/SelectLongproof.v | |
| parent | 6a3f3a62452670380827f9e39dd28c5092741099 (diff) | |
| download | compcert-kvx-f1d3dbb3fa70233d1ad83ae88876dd384346a16a.tar.gz compcert-kvx-f1d3dbb3fa70233d1ad83ae88876dd384346a16a.zip | |
Changed ptr64 to be always true
Diffstat (limited to 'mppa_k1c/SelectLongproof.v')
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 78a1935d..511dee92 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -123,7 +123,6 @@ Proof. predSpec Int64.eq Int64.eq_spec n Int64.zero. subst. exists x; split; auto. destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto. - destruct Archi.ptr64; auto. destruct (addlimm_match a); InvEval. - econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto. - econstructor; split. EvalOp. simpl; eauto. @@ -169,7 +168,6 @@ Proof. destruct Archi.ptr64 eqn:SF; auto. apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. rewrite (Ptrofs.add_commut (Ptrofs.of_int64 n1)), Ptrofs.add_assoc. f_equal. auto with ptrofs. - destruct Archi.ptr64 eqn:SF; auto. - subst. econstructor; split. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto. destruct sp; simpl; auto. @@ -177,7 +175,6 @@ Proof. destruct Archi.ptr64 eqn:SF; auto. apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. f_equal. rewrite Ptrofs.add_commut. auto with ptrofs. - destruct Archi.ptr64 eqn:SF; auto. - subst. replace (Val.addl (Val.addl v1 (Vlong n1)) y) with (Val.addl (Val.addl v1 y) (Vlong n1)). @@ -346,7 +343,6 @@ Proof. subst x. destruct v1; simpl; auto. simpl in B2; inv B2. simpl in B3; inv B3. rewrite Int64.mul_add_distr_l. rewrite (Int64.mul_commut n). auto. - destruct Archi.ptr64; simpl; auto. - apply eval_mullimm_base; auto. Qed. |