AdaCore Blog

GNATprove Tips and Tricks: Keeping Justifications Up-To-Date

by Yannick Moy

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.

Posted in #Formal Verification    #SPARK   

About Yannick Moy

Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a product he presents in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.