As a reader of this blog, you probably know that SPARK, to prove the absence of runtime errors in SPARK programs, translates the program into logical formulas that are then passed to powerful tools called SMT-solvers, that can prove the validity of the logical formulas. Simply put, for every check in your SPARK program, the tool generates a logical formula such that, if the SMT solver manages to prove it, the runtime check cannot happen.

The CodePeer tool for the static analysis of Ada programs functions in a vastly different way: It tracks the ranges of variables and expressions in your program.  When it encounters a runtime check (which often can also be expressed as a range), it will verify if the range of the variable and the range of the check allow for a potential runtime failure or not.

Though the applied techniques and use cases of CodePeer and SPARK are very different, ultimately, both tools will analyse the user code and try, for each potential runtime check, to prove that it cannot happen. If they fail to achieve this proof, a message will be issued to the user.  We always felt that there was some kind of synergy possible between CodePeer and SPARK, but we never quite saw how they would fit together, given their very different use cases and underlying techniques.

However, with the SPARK 17.1 release, we have finally brought the two technologies together.  In hindsight, the idea is very simple, but isn't it always like that?  We simply run the CodePeer tool as part of the SPARK analysis. Every check that has already identified as "cannot fail" by the CodePeer tool is not translated to logical formulas, and directly reported as proved.  From the user point of view, CodePeer becomes simply another proof tool.

In our tests, we have found CodePeer to be very effective. It quickly discharges all the simple runtime checks that can be proved simply by looking at the ranges of the involved variables and expressions.  It is particularly efficient when applied to runtime checks involving floating point variables.

Starting from SPARK Pro version 17.1 targeted for release in February, the CodePeer engine will be part of the SPARK Pro package.  It can be enabled on the command line with the switch "--codepeer=on", or by selecting the corresponding checkbox in the GPS and GNATBench plug-ins.

Note that CodePeer and SPARK are still separate products, because, as mentioned above, they cater to different use cases.

For more information, see the SPARK User's Guide.