diff options
| author | Yannick Moy <moy@adacore.com> | 2021-12-03 16:23:01 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-01-06 17:11:32 +0000 |
| commit | 4e5e43e8ca4f059c61bb1fccbf804bbce7375f5b (patch) | |
| tree | f459c871617ad5a7cdf63de8c3937e7c9f1a7db4 /gcc | |
| parent | 4458909a806825bc9a74b69e14c7fb88a551b800 (diff) | |
| download | gcc-4e5e43e8ca4f059c61bb1fccbf804bbce7375f5b.zip gcc-4e5e43e8ca4f059c61bb1fccbf804bbce7375f5b.tar.gz gcc-4e5e43e8ca4f059c61bb1fccbf804bbce7375f5b.tar.bz2 | |
[Ada] Justify false positive message from CodePeer analysis of GNAT
gcc/ada/
* libgnat/s-exponu.adb (Exponu): Add annotation.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/libgnat/s-exponu.adb | 3 |
1 files changed, 3 insertions, 0 deletions
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 |