| commit | f9a68b454743fffe07fb51ed735510c2178ba14c | |
| author | Sheri Bernstein <bernstein@adacore.com> | |
| Thu, 3 Aug 2023 12:38:53 +0000 (3 12:38 +0000) | ||
| committer | Marc Poulhiès <poulhies@adacore.com> | |
| Tue, 5 Sep 2023 11:05:12 +0000 (5 13:05 +0200) | ||
| tree | 6b173771600c10ae81c9e30cbde41e7ff7923d2d | treesnapshot (tar.gz zip) |
| parent | 17fcc7df64b5b6574e8dd24095a0f146382e62c3 | commitdiff |
ada: Remove GNATcheck violations
Use pragma Annotate to exempt GNATcheck violations that are related
to proof code. Specifically, exempt rules "Metrics_LSLOC" and
"Metrics_Cyclomatic_Complexity" whose limits are exceeded due to
proof code, and exempt rule "Discriminated_Records" for a variant record
that is only used in proof code.
gcc/ada/
* libgnat/s-aridou.adb: Add pragma to exempt Metrics_LSLOC.
(Double_Divide): Add pragma to exempt
Metrics_Cyclomatic_Complexity.
(Scaled_Divide): Likewise.
* libgnat/s-vauspe.ads (Uns_Option): Add pragma to exempt
Discriminated_Records.
Use pragma Annotate to exempt GNATcheck violations that are related
to proof code. Specifically, exempt rules "Metrics_LSLOC" and
"Metrics_Cyclomatic_Complexity" whose limits are exceeded due to
proof code, and exempt rule "Discriminated_Records" for a variant record
that is only used in proof code.
gcc/ada/
* libgnat/s-aridou.adb: Add pragma to exempt Metrics_LSLOC.
(Double_Divide): Add pragma to exempt
Metrics_Cyclomatic_Complexity.
(Scaled_Divide): Likewise.
* libgnat/s-vauspe.ads (Uns_Option): Add pragma to exempt
Discriminated_Records.
| gcc/ada/libgnat/s-aridou.adb | diffblobblamehistory | |
| gcc/ada/libgnat/s-vauspe.ads | diffblobblamehistory |