CodePeer is a source code analyzer that detects run-time and logic errors in Ada programs. Serving as an efficient and accurate code reviewer — in effect an expert assistant — 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.
CodePeer, developed in partnership with SofCheck Inc, is a standalone tool that may be used with any Ada compiler or fully integrated into the GNAT Pro development environment to significantly improve the soundess of code.
- Finds potential bugs and vulnerabilities early, when they are less expensive to correct
- Expedites code review and significantly increases the productivity of human review
- Detects and removes latent bugs when used retrospectively on existing code
- Reduces effort needed for safety or security certification
- Improves code quality u Works on partially complete programs
- Exploits multi-core CPUs for efficiency and allows performance tuning based on memory and speed of developer’s machine
- Uses static control-flow, data-flow, and possible-value-set propagation techniques to detect errors before program execution
- Mathematically analyzes every line of code without executing the program, considering all combinations of program input across all paths within the program
- Analyzes programs for a wide range of flaws (including use of uninitialized data, pointer misuse, buffer overflow, numeric overflow, division by zero, dead code, concurrency faults)
- Identifies not only where a failure could occur, but also where the bad values originate
- Detects code that, although syntactically and semantically correct, is performing a suspect computation (such as assigning to a variable that is never subsequently referenced or testing a condition that always evaluates to the same true or false value)
- Automatically generates both human-readable and machine-readable component specifications (preconditions and postconditions, inputs and outputs, heap allocations)