diff mbox series

[Ada] Add pragma Annotate for CodePeer analysis

Message ID 20211202162904.GA2159924@adacore.com
State New
Headers show
Series [Ada] Add pragma Annotate for CodePeer analysis | expand

Commit Message

Pierre-Marie de Rodat Dec. 2, 2021, 4:29 p.m. UTC 
CodePeer issues a spurious message on the analysis of the loop variant
in s-widthi.adb. Similarly to the same for s-widthu.adb, add a pragma
Annotate to justify this message.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* libgnat/s-widthi.adb: Add pragma Annotate.
diff mbox series

Patch

diff --git a/gcc/ada/libgnat/s-widthi.adb b/gcc/ada/libgnat/s-widthi.adb
--- a/gcc/ada/libgnat/s-widthi.adb
+++ b/gcc/ada/libgnat/s-widthi.adb
@@ -163,6 +163,9 @@  begin
          pragma Loop_Invariant (Pow = Big_10 ** (W - 2));
          pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow);
          pragma Loop_Variant (Decreases => T);
+         pragma Annotate
+           (CodePeer, False_Positive,
+            "validity check", "confusion on generated code");
       end loop;
 
       declare