diff options
| author | Yannick Moy <moy@adacore.com> | 2023-06-29 12:14:39 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-07-10 14:41:39 +0200 |
| commit | bcc2c7fa6ed8b7dbb0e3ba11e40958f1b99b83d0 (patch) | |
| tree | 1d0f77a2dffab2c1e3662ba947c972ab94b16861 | |
| parent | 9105cd9062520969092fe4ecb3ce5ef34b2dfaaf (diff) | |
| download | gcc-bcc2c7fa6ed8b7dbb0e3ba11e40958f1b99b83d0.zip gcc-bcc2c7fa6ed8b7dbb0e3ba11e40958f1b99b83d0.tar.gz gcc-bcc2c7fa6ed8b7dbb0e3ba11e40958f1b99b83d0.tar.bz2 | |
ada: Simplify assertion to remove CodePeer message
CodePeer is correctly warning on a test always true in an assertion.
It can be rewritten without loss of proof to avoid that message.
gcc/ada/
* libgnat/s-aridou.adb (Lemma_Powers_Of_2_Commutation): Rewrite
assertion.
| -rw-r--r-- | gcc/ada/libgnat/s-aridou.adb | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 7ebf868..2f1fbd5 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -1456,9 +1456,7 @@ is pragma Assert (Big (Double_Uns'(2))**M = Big_2xx (M)); end if; else - pragma Assert - (Big (Double_Uns'(2))**M = - (if M < Double_Size then Big_2xx (M) else Big_2xxDouble)); + pragma Assert (Big (Double_Uns'(2))**M = Big_2xx (M)); end if; end Lemma_Powers_Of_2_Commutation; |