GNATprove supports the suppression of warnings and justification of check messages with respectively pragma Warnings and pragma Annotate inserted in the source code. This allows users to analyze false alarms produced by the tool once, and make sure that the same alarms won't be issued in every future analysis. But these justifications may become useless in various cases:

1. Due to a change in code, the warning/check message is not present anymore.
2. Due to a change in contracts, GNATprove can now show there is no possible problem.
3. Due to an improvement in a new version of GNATprove, the warning/check message is not emitted anymore.

Keeping useless justifications in the code is confusing (for maintenance and reviews), so it should be avoided as much as possible. To help with that, GNATprove now issues a warning when a pragma Warnings or pragma Annotate used to justify messages is useless, that is, when GNATprove never attempts to issue such a message.

For pragma Annotate, GNATprove performs this detection by default.

For pragma Warnings, GNATprove performs this detection when the switch -gnatw.w is used. This is similar to the detection of useless pragma Warnings in the GNAT compiler. To distinguish between pragma Warnings which apply to both GNAT and GNATprove or only one of these tools, it is now possible to specify the name of the tool as a first argument of the pragma. See SPARK User's Guide for examples.