From 4e5e43e8ca4f059c61bb1fccbf804bbce7375f5b Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 3 Dec 2021 16:23:01 +0100 Subject: [PATCH] [Ada] Justify false positive message from CodePeer analysis of GNAT gcc/ada/ * libgnat/s-exponu.adb (Exponu): Add annotation. --- gcc/ada/libgnat/s-exponu.adb | 3 +++ 1 file changed, 3 insertions(+) diff --git a/gcc/ada/libgnat/s-exponu.adb b/gcc/ada/libgnat/s-exponu.adb index 06ed509..2885d6b 100644 --- a/gcc/ada/libgnat/s-exponu.adb +++ b/gcc/ada/libgnat/s-exponu.adb @@ -64,6 +64,9 @@ begin pragma Loop_Invariant (Exp > 0); pragma Loop_Invariant (Result * Factor ** Exp = Left ** Right); pragma Loop_Variant (Decreases => Exp); + pragma Annotate + (CodePeer, False_Positive, + "validity check", "confusion on generated code"); if Exp rem 2 /= 0 then pragma Assert -- 2.7.4