AdaCore CodePeer Source Code Analysis Tool for Ada
AdaCore introduced CodePeer analysis tool. CodePeer can be used either as a standalone tool or fully integrated into the GNAT Pro Ada development environment. It is highly flexible. Performance can be tuned based on the memory and speed available on the developer’s machine. CodePeer can also efficiently exploit multi-core CPUs. The source code tool can be run on partially complete programs and it does not require stubs or drivers. CodePeer is available immediately.
What is AdaCore CodePeer?
CodePeer is a source code analysis tool that detects run-time and logic errors in Ada programs. 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. CodePeer also produces a detailed analysis of each subprogram, including pre- and postconditions. 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.
What kind of errors does CodePeer detect?
CodePeer analyses 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). CodePeer identifies errors statically, without running the program. The tool 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.
How does AdaCore CodePeer work?
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. CodePeer 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.
More info: AdaCore
If you are familiar with RSS feeds, you can also sign up for our free blog feed. Our RSS feed is updated in real-time while our newsletter is updated daily.