From 7d5db993033ce049776fa290ae1ebc6051dea0f3 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Sat, 17 Aug 2019 10:10:42 +0200 Subject: Fix compile for architectures other than AArch64 (#192) Some changes were not correctly propagated to all architectures. --- backend/SelectDivproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend') diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 334bedf6..c57d3652 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -835,7 +835,7 @@ Proof. assert (A0: eval_expr ge sp e m le (Eletvar O) (Vlong x)). { constructor; auto. } exploit eval_mullhs. try apply HELPERS. eexact A0. instantiate (1 := Int64.repr M). intros (v1 & A1 & B1). - exploit eval_addl. try apply HELPERS. eexact A1. eexact A0. intros (v2 & A2 & B2). + exploit eval_addl. auto. eexact A1. eexact A0. intros (v2 & A2 & B2). exploit eval_shrluimm. try apply HELPERS. 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) @@ -844,7 +844,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. try apply HELPERS. eexact A4. instantiate (1 := Int.repr p). intros (v5 & A5 & B5). - exploit eval_addl. try apply HELPERS. 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. } -- cgit