[gcc r12-6294] [Ada] Justify false positive message from CodePeer analysis of GNAT

Pierre-Marie de Rodat pmderodat@gcc.gnu.org
Thu Jan 6 17:13:11 GMT 2022


https://gcc.gnu.org/g:4e5e43e8ca4f059c61bb1fccbf804bbce7375f5b

commit r12-6294-g4e5e43e8ca4f059c61bb1fccbf804bbce7375f5b
Author: Yannick Moy <moy@adacore.com>
Date:   Fri Dec 3 16:23:01 2021 +0100

    [Ada] Justify false positive message from CodePeer analysis of GNAT
    
    gcc/ada/
    
            * libgnat/s-exponu.adb (Exponu): Add annotation.

Diff:
---
 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 06ed5099c25..2885d6b4f19 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


More information about the Gcc-cvs mailing list