diff options
| author | Yannick Moy <moy@adacore.com> | 2022-07-04 10:49:02 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-07-13 10:01:15 +0000 |
| commit | b872d3fe67b54fef84ccafc7d39f1017a68332c2 (patch) | |
| tree | 51ea86adbd6e103fe761eccf384081a9da82136e /gcc/ada/libgnat | |
| parent | 7a03001cd2dadbe845f109382e4c0dc2dbb50820 (diff) | |
| download | gcc-b872d3fe67b54fef84ccafc7d39f1017a68332c2.zip gcc-b872d3fe67b54fef84ccafc7d39f1017a68332c2.tar.gz gcc-b872d3fe67b54fef84ccafc7d39f1017a68332c2.tar.bz2 | |
[Ada] Fix automatic proof on System.Arith_32
gcc/ada/
* libgnat/s-arit32.adb (Scaled_Divide32): Add an assertion, move
the call of Prove_Sign_R around.
Diffstat (limited to 'gcc/ada/libgnat')
| -rw-r--r-- | gcc/ada/libgnat/s-arit32.adb | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb index 6dac572..c3d9f6a 100644 --- a/gcc/ada/libgnat/s-arit32.adb +++ b/gcc/ada/libgnat/s-arit32.adb @@ -541,8 +541,10 @@ is end if; end if; + pragma Assert (In_Int32_Range (Big_Q)); pragma Assert (Big (Qu) = abs Big_Q); pragma Assert (Big (Ru) = abs Big_R); + Prove_Sign_R; -- Set final signs (RM 4.5.5(27-30)) @@ -563,7 +565,6 @@ is Q := (if Z > 0 then To_Neg_Int (Qu) else To_Pos_Int (Qu)); end if; - Prove_Sign_R; Prove_Signs; end Scaled_Divide32; |