From bcc2c7fa6ed8b7dbb0e3ba11e40958f1b99b83d0 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 29 Jun 2023 12:14:39 +0000 Subject: [PATCH] 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. --- 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 7ebf8682b320..2f1fbd554531 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.47.2