diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-25 15:11:30 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-25 15:11:30 +0200 |
commit | 1f004665758e26e6e48d13f5702fe55af8944448 (patch) | |
tree | e3ccaee73c86ec1aef94ef66341610ed4436f93a /backend/SelectDivproof.v | |
parent | 271a6f98809fbeac6cb04fb29fccbcf9c1e18335 (diff) | |
download | compcert-1f004665758e26e6e48d13f5702fe55af8944448.tar.gz compcert-1f004665758e26e6e48d13f5702fe55af8944448.zip |
Update ARM port. Not tested yet.
Diffstat (limited to 'backend/SelectDivproof.v')
-rw-r--r-- | backend/SelectDivproof.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 41db3c70..3180a55d 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -713,7 +713,8 @@ Lemma eval_modl_from_divl: Proof. unfold modl_from_divl; intros. exploit eval_mullimm; eauto. instantiate (1 := n). intros (v1 & A1 & B1). - exploit (eval_subl prog sp e m le (Eletvar O)). constructor; eauto. eexact A1. + assert (A0: eval_expr ge sp e m le (Eletvar O) (Vlong x)) by (constructor; auto). + exploit eval_subl; auto. eexact A0. eexact A1. intros (v2 & A2 & B2). simpl in B1; inv B1. simpl in B2; inv B2. exact A2. Qed. @@ -798,7 +799,7 @@ Proof. assert (A0: eval_expr ge sp e m le (Eletvar O) (Vlong x)). { constructor; auto. } exploit eval_mullhs. eauto. eexact A0. instantiate (1 := Int64.repr M). intros (v1 & A1 & B1). - exploit eval_addl. eexact A1. eexact A0. intros (v2 & A2 & B2). + exploit eval_addl; auto. eexact A1. eexact A0. intros (v2 & A2 & B2). exploit eval_shrluimm. eauto. eexact A0. instantiate (1 := Int.repr 63). intros (v3 & A3 & B3). set (a4 := if zlt M Int64.half_modulus then mullhs (Eletvar 0) (Int64.repr M) @@ -807,7 +808,7 @@ Proof. assert (A4: eval_expr ge sp e m le a4 v4). { unfold a4, v4; destruct (zlt M Int64.half_modulus); auto. } exploit eval_shrlimm. eauto. eexact A4. instantiate (1 := Int.repr p). intros (v5 & A5 & B5). - exploit eval_addl. eexact A5. eexact A3. intros (v6 & A6 & B6). + exploit eval_addl; auto. eexact A5. eexact A3. intros (v6 & A6 & B6). assert (RANGE: forall x, 0 <= x < 64 -> Int.ltu (Int.repr x) Int64.iwordsize' = true). { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto. assert (64 < Int.max_unsigned) by (compute; auto). omega. } |