AdaCore, a leading supplier of Ada development tools and support services, announced the release ofCodePeer,
a source code analysis tool that detects run-time and logic errors in
Ada programs.
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 postconditions. 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. CodePeer can be used both during system development − to
prevent errors from being introduced or as part of a systematic code
review process to dramatically increase the efficiency of human review
− and retrospectively on existing code, to detect and remove latent
bugs.
Developed by AdaCore in partnership withSofCheck, Inc., CodePeer can be used either as a standalone tool or fully integrated into theGNAT ProAda
development environment. It is highly flexible, with performance that
can be tuned based on the memory and speed available on the developer’s
machine, and can efficiently exploit multi-core CPUs. CodePeer can be
run on partially complete programs; it does not require stubs or
drivers.
CodePeer analyzes programs for a wide range of flaws including use
of uninitialized data, pointer misuse, buffer overflow, numeric
overflow, division by zero, dead code, and concurrency faults (race
conditions). These sorts of errors can be difficult and expensive to
detect and correct with conventional debugging, but CodePeer identifies
them statically, without running the program, and determines not only
where the failure could occur, but identifies where the bad values
originate, be it within the current subprogram or from some distant
subprogram that reached the point of failure through a series of calls.
CodePeer also looks for code that, although syntactically and
semantically correct, is performing a suspect computation, such as an
assignment to a variable that is never subsequently referenced, or a
conditional test that always evaluates to the same true or false value.
“Even the best programmers using the best programming languages will
sometimes make mistakes,” said Robert Dewar, President and CEO of
AdaCore. “The key is to detect and correct errors early, and, thanks to
our partnership with SofCheck, CodePeer is now available for precisely
that purpose. We expect this tool to be especially valuable to our
customers with safety-critical or high-security requirements, since
CodePeer can identify potential hazards and vulnerabilities.”
Internally CodePeer uses static control-flow, data-flow, and value
propagation techniques to identify possible errors. It mathematically
analyzes every line of code without executing the program, considering
all combinations of program input across all paths within the program.
It automatically generates both human-readable and machine-readable
component specifications in the form of preconditions, postconditions,
inputs, outputs, and heap allocations, which along with the error
messages can be displayed graphically or as in-line comments in the
source code listing to help immediately pinpoint the root cause of any
defect. In a multi-threaded system CodePeer identifies where race
conditions might occur. To increase performance and usability it
internally maintains a historical error database, which allows it to
highlight just the new coding problems and to track trends across
multiple analyses.
