From: Yannick Moy Date: Fri, 26 Nov 2021 08:32:09 +0000 (+0100) Subject: [Ada] Add pragma Annotate for CodePeer analysis X-Git-Tag: basepoints/gcc-13~2572 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=ce79e7e24acdc83620782dae9b954b1ad2bdb988;p=thirdparty%2Fgcc.git [Ada] Add pragma Annotate for CodePeer analysis gcc/ada/ * libgnat/s-widthi.adb: Add pragma Annotate. --- diff --git a/gcc/ada/libgnat/s-widthi.adb b/gcc/ada/libgnat/s-widthi.adb index 55a94ecfc10c..e47c8c13f271 100644 --- 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