Developing in Ada? – static-analysis and dynamic-analysis tools get an update
CodePeer 2.3 for the automated review and validation of Ada source code assesses potential bugs before program execution to find errors early in the development life cycle. It also performs impact and vulnerability analysis when existing code is modified, and, using control-flow, data-flow, and other advanced static analysis techniques, the tool detects problems that would otherwise only be found through labour-intensive debugging.
The latest update to CodePeer delivers more precise diagnostic messages and fewer “false positives”. It also includes an independent Ada front end, and provides better integration with AdaCore’s two IDEs: GNAT Programming Studio (GPS) and GNATbench (the GNAT Pro Ada plug-in for Eclipse and Wind River Systems Workbench). Other enhancements include support for floating point overflow on unconstrained types, the ability to supply target configuration files, and improved support for existing codebases in Ada 83. Improved message review capabilities are now available through pragma Annotate, and the tool provides new warnings when a formal parameter could be declared with a more restrictive mode.
CodePeer is fully integrated into the GNAT Pro development environment and comes with a number of complementary static analysis tools common to the technology – a coding standard verification tool (GNATcheck), a source code metric generator (GNATmetric), a semantic analyzer, and a document generator.
Serving as an efficient and accurate code reviewer, CodePeer identifies constructs that are likely to lead to run-time errors such as buffer overflows, and it flags legal but suspect code, typical of logic errors. Going well beyond the capabilities of typical static analysis tools, CodePeer also produces a detailed analysis of each subprogram, including pre- and post-conditions. Such an analysis makes it easier to find potential bugs and vulnerabilities early: if the implicit specification deduced by CodePeer does not match the component’s requirements, a reviewer is alerted immediately to a likely logic error. During system development, CodePeer can help prevent errors from being introduced, and it can also be used as part of a systematic code review process to dramatically increase the efficiency of human review. CodePeer can be used retrospectively on existing code, to detect and remove latent bugs.
Dynamic analysis
Moving on to runnning code, AdaCore has a new version of its GNATcoverage Dynamic Analysis Tool, a coverage tool that supports all levels of safety certification and adds hardware probing. Functionality.
GNATcoverage 1.2 does not require instrumentation of the executable, and this new product release supports usage with an iSystem hardware probe generating Nexus trace data, as well as usage with Valgrind on Linux. GNATcoverage 1.2 supports Ada 95, Ada 2005 and many new features in Ada 2012. It can also be used for the upcoming SPARK 2014 revision and includes Beta support for C. Other enhancements include generation of coverage information for generics on a per-instance basis, and improved HTML output (sortable columns, project awareness). The tool is now integrated with the GNAT Pro development environment.
Qualification material is available to support GNATcoverage usage as a verification tool (DO-178B) or a tool at TQL-5 (DO-178C). It can be used as part of the verification process for systems that need to be certified up to Level A, and can thus supply analysis up to Modified Condition/Decision Coverage (MCDC). GNATcoverage can also be used for railway applications that need to comply with EN-50128:2011 (T2).
AdaCore; www.adacore.com
If you enjoyed this article, you will like the following ones: don't miss them by subscribing to :
