From: Yannick Moy <m...@adacore.com>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/libgnat/s-aridou.adb | 4 +---
1 file changed, 1 insertion(+), 3 deletions(-)
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index 7ebf8682b32..2f1fbd55453 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;
--
2.40.0
