From e9f40aaca38ba81f3e9e5c0a5e03de9fa074d838 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 10 Jun 2021 09:52:47 +0200 Subject: Int.sign_ext_shr_shl: weaker hypothesis Works also for sign_ext 32. ARM, RISC-V: adapt Asmgenproof1 accordingly --- arm/Asmgenproof1.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm') diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index b94964a0..6f0482dc 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -1218,7 +1218,7 @@ Proof. split. unfold rs2; Simpl. unfold rs1; Simpl. unfold Val.shr, Val.shl; destruct (rs x0); auto. change (Int.ltu (Int.repr 24) Int.iwordsize) with true; simpl. - f_equal. symmetry. apply (Int.sign_ext_shr_shl 8). compute; auto. + f_equal. symmetry. apply (Int.sign_ext_shr_shl 8). compute; intuition congruence. intros. unfold rs2, rs1; Simpl. (* Ocast16signed *) destruct Archi.thumb2_support. @@ -1231,7 +1231,7 @@ Proof. split. unfold rs2; Simpl. unfold rs1; Simpl. unfold Val.shr, Val.shl; destruct (rs x0); auto. change (Int.ltu (Int.repr 16) Int.iwordsize) with true; simpl. - f_equal. symmetry. apply (Int.sign_ext_shr_shl 16). compute; auto. + f_equal. symmetry. apply (Int.sign_ext_shr_shl 16). compute; intuition congruence. intros. unfold rs2, rs1; Simpl. (* Oaddimm *) generalize (addimm_correct x x0 i k rs m). -- cgit