diff options
| author | Yannick Moy <moy@adacore.com> | 2022-04-20 09:39:11 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-30 08:29:01 +0000 |
| commit | 1ea22318caf52a98b32f8ef4e155376e7751db4b (patch) | |
| tree | 0695039fc78b5643e05c9ead47ad0bb6b271d11f | |
| parent | 5b7630f2f266346173eb2172a9a96e925010afc5 (diff) | |
| download | gcc-1ea22318caf52a98b32f8ef4e155376e7751db4b.zip gcc-1ea22318caf52a98b32f8ef4e155376e7751db4b.tar.gz gcc-1ea22318caf52a98b32f8ef4e155376e7751db4b.tar.bz2 | |
[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.
| -rw-r--r-- | gcc/ada/libgnat/s-arit32.adb | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb index baec78a..3d500ac 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); |