diff options
| author | Yannick Moy <moy@adacore.com> | 2021-11-26 09:32:09 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-12-02 16:26:29 +0000 |
| commit | ce79e7e24acdc83620782dae9b954b1ad2bdb988 (patch) | |
| tree | da7da021ebea8397b6510e0d0f6bb15ae9f3bd69 /gcc | |
| parent | 3a54dfa801a1cfb387c8c43e7610b11905db505c (diff) | |
| download | gcc-ce79e7e24acdc83620782dae9b954b1ad2bdb988.zip gcc-ce79e7e24acdc83620782dae9b954b1ad2bdb988.tar.gz gcc-ce79e7e24acdc83620782dae9b954b1ad2bdb988.tar.bz2 | |
[Ada] Add pragma Annotate for CodePeer analysis
gcc/ada/
* libgnat/s-widthi.adb: Add pragma Annotate.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/libgnat/s-widthi.adb | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/gcc/ada/libgnat/s-widthi.adb b/gcc/ada/libgnat/s-widthi.adb index 55a94ec..e47c8c13 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 |