diff mbox series

[COMMITTED] ada: Simplify assertion to remove CodePeer message

Message ID 20230710124427.2263633-1-poulhies@adacore.com
State Unresolved
Headers
Series [COMMITTED] ada: Simplify assertion to remove CodePeer message |

Checks

Context Check Description
snail/gcc-patch-check warning Git am fail log

Commit Message

Marc Poulhiès July 10, 2023, 12:44 p.m. UTC 
  From: Yannick Moy <moy@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 mbox series

Patch

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;