CodePeer by AdaCore

Software Validation and Verification

Product Description

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.

Benefits

- 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

Features

- 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)  

CodePeer

Market Segment(s)

• Embedded

ARM Processor(s)

• Cortex-A53
• Cortex-A57
• ARMv8

 Contact Us