CodePeer generates the contract for a procedure when none exists, allowing a developer to see what the procedure will actually do with inputs and outputs. Click here for expanded view. (Image courtesy of Adacore)

Best of 2015: CodePeer SPARKS Ada

Dec. 4, 2015

Adacore’s CodePeer takes verification of Ada code to the next level.

Some tools need time before they become refined and really useful. That was the case with Gumstix’s Geppetto (see “Create Custom Capes Fast and Easy” on Electronic Design). Geppetto recently added support for processors and popular platforms like Raspberry Pi to the PCB design and delivery system.

This is also the case for Adacore’s CodePeer. CodePeer analyzes Ada programs looking for run-time and logic errors. It is similar to many static analysis programs designed to identify errors in C, C++, and Java applications, but CodePeer has an advantage. Ada tends to be more rigorous with programmers with the advantage of allowing developers more precise control over the application. The Ada 2012 standard goes farther by providing support for contracts (see “Ada 2012: The Joy of Contracts” on Electronic Design).

A more restricted subset of Ada 2012 is SPARK. It allows formal methods to be used in proving a program will meet the specified requirements that are specified using Ada contracts. Some sample output from CodePeer (see the figure) highlights how this works.

Ada 2012 contracts allow definitions for procedure, modules, and other code entities to include pre-conditions and post-conditions like those shown in the example. In this case, the argument N must be a positive Natural number. A zero of negative value would generate a runtime error.

Electronicdesign Com Sites Electronicdesign com Files Uploads 2015 06 Capture Format

CodePeer can generate the contract information and will compare it with any contracts that programmer provides as well. The CodePeer contract could also be moved into the code as well, making the code more robust since changing the code without changing the contract would allow the system to detect an error where the new code now conflicts with the promised contract.

Of course, CodePeer also detects conflicts between its actual contract and any the programmer provides. It also flags errors so that even a banker could not write a contract that would work.

Any static analysis program including CodePeer can generate false positives. It tends to do better than other tools because of the language being analyzed. Languages like C allow programmers to easily shoot themselves in the proverbial foot and they typically do so, much to the chagrin of users of the programs.

There are many myths about Ada and it does not command the interest that C or C++ does in the embedded realm, but the rise of the Internet of Things (IoT) —along with its security and reliability issues—should bring Ada into a better light. Ada and CodePeer can have a major impact in the quality of any code for IoT or other applications. Ada has moved past its military and aviation roots to other transportation arenas, including trains and automotive.