From f849a03bc11b2bc3c6373213afc2a7023c636679 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 22 Jun 2016 10:38:21 +0200 Subject: Improved handling of "rotate left" and "rotate right" operators - Values: "rol" and "ror" are defined even if their second argument is not in the [0,31] range (for consistency with "rolm" and because the semantics is definitely well defined in this case). - NeedDomain: more precise analysis of "rol" and "rolm", could benefit the PowerPC port. --- arm/ConstpropOpproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'arm/ConstpropOpproof.v') diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 6f6afa8a..0b7643c6 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -98,7 +98,7 @@ Ltac SimplVM := Lemma eval_static_shift_correct: forall s n, eval_shift s (Vint n) = Vint (eval_static_shift s n). Proof. - intros. destruct s; simpl; rewrite s_range; auto. + intros. destruct s; simpl; rewrite ? s_range; auto. Qed. Lemma cond_strength_reduction_correct: -- cgit