From 1ea22318caf52a98b32f8ef4e155376e7751db4b Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 20 Apr 2022 09:39:11 +0000 Subject: [PATCH] [Ada] Adapt proof of runtime unit s-arit32 After changes in GNATprove, adapt proof. Simply move an assertion up before it is first needed here. gcc/ada/ * libgnat/s-arit32.adb (Scaled_Divide32): Move assertion up. --- gcc/ada/libgnat/s-arit32.adb | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb index baec78a34750..3d500ac8fad1 100644 --- a/gcc/ada/libgnat/s-arit32.adb +++ b/gcc/ada/libgnat/s-arit32.adb @@ -474,6 +474,7 @@ is D := Uns64 (Xu) * Uns64 (Yu); + Lemma_Abs_Mult_Commutation (Big (X), Big (Y)); pragma Assert (Mult = Big (D)); Lemma_Hi_Lo (D, Hi (D), Lo (D)); pragma Assert (Mult = Big_2xx32 * Big (Hi (D)) + Big (Lo (D))); @@ -508,7 +509,6 @@ is Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z)); Lemma_Abs_Rem_Commutation (Big (X) * Big (Y), Big (Z)); - Lemma_Abs_Mult_Commutation (Big (X), Big (Y)); Lemma_Abs_Commutation (X); Lemma_Abs_Commutation (Y); Lemma_Abs_Commutation (Z); -- 2.47.2