aboutsummaryrefslogtreecommitdiff
path: root/gcc
diff options
context:
space:
mode:
authorArnaud Charlet <charlet@adacore.com>2021-10-19 12:44:17 -0400
committerPierre-Marie de Rodat <derodat@adacore.com>2021-10-25 15:07:20 +0000
commitc652a33260b19ac1ee3cd15cadb4b3499ac587f9 (patch)
tree6047165429127db4142d50fa47714400c7442c88 /gcc
parent67397bb9888e72fe300746ee9c77b83ce367b733 (diff)
downloadgcc-c652a33260b19ac1ee3cd15cadb4b3499ac587f9.zip
gcc-c652a33260b19ac1ee3cd15cadb4b3499ac587f9.tar.gz
gcc-c652a33260b19ac1ee3cd15cadb4b3499ac587f9.tar.bz2
[Ada] Shutdown codepeer message
gcc/ada/ * libgnat/s-widthu.adb: Add pragma Annotate.
Diffstat (limited to 'gcc')
-rw-r--r--gcc/ada/libgnat/s-widthu.adb5
1 files changed, 4 insertions, 1 deletions
diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb
index e0e4d17..fce8c7a 100644
--- a/gcc/ada/libgnat/s-widthu.adb
+++ b/gcc/ada/libgnat/s-widthu.adb
@@ -134,10 +134,13 @@ begin
W := W + 1;
Pow := Pow * 10;
- pragma Loop_Variant (Decreases => T);
pragma Loop_Invariant (W in 3 .. Max_W + 3);
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