The GNAT compiler, like many other compilers, has three different types of messages: errors, warnings and info messages:

• Errors are used to indicate serious problems with the code which prevent the compiler from generating code for the program: syntax or typing errors, combinations of features which are not allowed by the language, etc.
• Warnings do not stop compilation (unless the user wants them to), but inform that some code probably doesn't do what the user wants. This can be a useless with clause, or a loop where the loop condition never changes, or many more.
• Finally the compiler issues info messages in certain situations, usually to better explain some warning or error message.

The GNAT compiler also provides a way to suppress certain classes of warnings or certain individual warnings. Errors cannot be suppressed.

Up until recently, the SPARK toolset copied this approach of errors, warnings and info messages and issued:

• info messages for proved checks
• warnings both for suspicious code (e.g. dead code, unused value of a variable) and some verification errors (variable uninitialized on some paths, failing run-time checks or assertions)
• errors, for illegal code and also for some verification errors (variable uninitialized on all paths)

The reason to make some verification results errors and some warnings was that some messages seemed more serious to us (like a variable which is uninitialized on all paths leading to the read) and for other messages the likelihood for false positives is relatively high, this is why we made all proof messages warnings. In this way, the user could accept these messages for example with pragma Warnings. As for compilation, error messages stop the analysis process.

However, this scheme was not satisfactory. The choice between warnings and errors was kind of arbitrary, but had a very important consequence: an error can never be justified and stops analysis completely. This was a problem because false positives could not be excluded even for this category, so this left the user without a way out except rewriting his code. We didn't want to make everything a warning either, because warnings always seem like the thing you can safely ignore.

In the 2015 SPARK Pro and GPL releases, this scheme will change. We now have added a fourth category of messages, and the tool now issues messages following these rules:

• info messages for proved checks
• warnings for suspicious code (e.g. dead code, unused value of a variable)
• checks for verification results which impact the soundness of the program (initialization of variables, possibly failing run-time checks and assertions)
• errors for legality problems in the code

The new category checks has been added to the output of the SPARK toolset. The idea is that if you have SPARK code without any errors (obviously) and without any check messages, then your code is safe and the analysis results are correct. You may still have suspicious situations, which are detected by a warning.

Check messages also come with a severity, which ranges from "low" through "medium" to "high". This is to align the GNATprove output a bit with the CodePeer tool for static analysis, where all messages also come with a severity, but also to recover to some extent the difference in likelihood for a message, which was previously expressed with the error/warning difference.

All check messages can be accepted/suppressed just like warnings, but using a different mechanism.

You can also check out the corresponding sections of the SPARK Toolset User's Guide. Finally note that this is an incompatible change with previous versions of the SPARK toolset.