1. Introduction

1.1. About CodePeer

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 performs line-by-line testing in a fully automated way, and guarantees full path coverage. CodePeer finds defects early in the development process in conjunction with compilation when they are least costly to repair. In addition, it should be run on existing code to find latent defects before they become a problem in the field.

CodePeer is designed to support large systems and to detect a wide range of programming errors such as misuse of pointers, indexing out of arrays, buffer overflows (a prevalent source of security storage leaks), numeric overflows, numeric wraparounds, and improper use of Application Programming Interfaces (APIs). It pinpoints the root cause of each error down to the source line of code.

Even in the absence of explicit errors, CodePeer provides a thorough characterization of every component of the system in terms of its inputs, outputs, heap object creations, the preconditions on the inputs necessary to preclude run-time failures, the presumptions about return values of external subprograms, and the postconditions that characterize the range of outputs.

One of the strengths of CodePeer is its ability to analyze partial systems (e.g. libraries, incomplete set of sources, etc.) and make reasonable assumptions about functions that are not visible.

Another strength is the historical database maintained by CodePeer which allows users to ignore initial messages on an existing code base, and concentrate on new messages only detected as part of code changes.

In addition, CodePeer supports analysis of Ada code written for many different Ada compilers via the configuration of a project file, see Project File Setup.

An analysis may be launched from the command line for easy scripting and automation, or interactively using GPS. Output is produced as text, html, and via a database.

For information about how CodePeer works internally, see How does CodePeer Work?.

For a high level comparison between SPARK and CodePeer, see What’s the Difference between CodePeer and SPARK?.

To get started quickly with CodePeer, see the CodePeer tutorial via e.g. GPS Help ‣ CodePeer ‣ CodePeer Tutorial menu.

You will also find several examples via the Help ‣ CodePeer ‣ Examples menu in GPS.

1.2. How to Install CodePeer

We recommend to first install GPS (and optionally GNAT), and then install CodePeer under the same location. Alternatively, you can install the GNATbench plug-in for Eclipse instead of GPS, using the Eclipse installation mechanism.

If however you choose to install CodePeer in a different location, prefer refer to Installation under different locations.

1.2.1. Installation under Windows

If not already done, first run the GPS installer by e.g. double clicking on gps-18.2-x86-windows-bin.exe and follow the instructions.

Then similarly run the CodePeer installer, by e.g. double clicking on codepeer-18.2-x86-windows-bin.exe.

You should have sufficient rights for installing the package (administrator or normal rights depending on whether it is installed for all users or a single user).

Be sure to change the default location so that both GPS and CodePeer are installed under the same location of your choice.

1.2.2. Installation under Unix

If not already done, you need to extract and install the GPS compressed tarball and then run the install, e.g:

$ gzip -dc gps-18.2-x86_64-linux-bin.tar.gz | tar xf -
$ cd gps-18.2-x86_64-linux-bin
$ ./doinstall

Then follow the instructions displayed.

Then do the same with the codepeer tarball, e.g.:

$ gzip -dc codepeer-18.2-x86_64-linux-bin.tar.gz | tar xf -
$ cd codepeer-18.2-x86_64-linux-bin
$ ./doinstall

Be sure to specify the same location chosen during the GPS installation.

Note that you need to have sufficient rights for installing the package at the chosen location (e.g. root rights for installing under /opt/codepeer).

1.2.3. Installation under different locations

If you decide to install GPS and CodePeer under different locations, you should also modify or set the following environment variable:

  • GPR_PROJECT_PATH, in order to analyze with CodePeer projects that depend on library projects installed with GNAT, such as GNATcoll;

On Windows, you can edit the value of GPR_PROJECT_PATH under the Environment Variables panel, and add to it the value of <GNAT install dir>\lib\gnat;<GNAT install dir>\share\gpr.

On Unix you can use, for instance, using Bourne-shell-compatible syntax:

$ GPR_PROJECT_PATH=<GNAT install dir>/lib/gnat:<GNAT install dir>/share/gpr:$GPR_PROJECT_PATH

or with C shell:

$ setenv GPR_PROJECT_PATH <GNAT install dir>/lib/gnat:<GNAT install dir>/share/gpr:$GPR_PROJECT_PATH