2. How to Run CodePeer

2.1. System Requirements

Static error detection is complex and time consuming, so CodePeer will benefit from all the speed (CPU) and memory (RAM) that can be made available. Dual core 2.0 GHz or greater CPUs can inspect about 1,000 lines of code per minute. A minimum of 2 GB of RAM per core is recommended. More complex analyses will require more memory. A recommended configuration for running CodePeer on large systems is an x86-64 machine running Linux 64bits or Windows 64bits with at least 8 cores and 16 GB of RAM. Slower machines can be used to analyze small subsystems, but a minimum of 1Ghz CPU and 2 GB of RAM is required.

In addition, if you want to perform global analysis using the -level max switch (complete analysis with no partitioning) you will need approximately 1 GB of RAM per 10K SLOC of code. In other words, in order to analyze 300K SLOC of code at -level max, you will need a 64bits configuration with at least 30 GB of RAM. Note that these numbers will vary depending on the complexity of your code. If your code is very simple, you will need less memory. On the other hand if your code is very complex, then you will likely need more memory.

2.2. Basic Project File Set Up

2.2.1. Basic Set Up

If not already done, create a GNAT project file (.gpr), as documented in the GPRbuild User’s Guide, section GNAT Project Manager. See also Project Attributes for optional project attributes to specify the output directories and other CodePeer switches in the project file directly.

Note that you can use the project wizard from GPS to create a project file interactively, via the menu File ‣ New Project.... In the dialog, see in particular the default option (Single Project).

If you want to get started quickly, and assuming a standard naming scheme using .ads/.adb lower case files and a single source directory, then your project file will look like:

project My_Project is
   for Source_Dirs use (".");
end My_Project;

saved in a file called my_project.gpr.

2.2.2. Configuring IDEs to Drive Tools

Note: if you are using GPS also with the GNAT compiler, you can skip this section.

If you are using CodePeer as a standalone tool without a GNAT installation, and want to use other tools from the CodePeer package (e.g. computation of metrics, coding standard checking), then you will need to add the following section to your project file:

for Target use "codepeer";

2.2.3. Simple Naming Scheme

If you are using a different naming scheme (than the default .ads/ .adb) for your source files, you will need to use either the simple approach designed in Simple Non Default Naming Scheme if it suits your project, or the more complex approach described in Arbitrary Naming Scheme.

2.2.3.1. Simple Non Default Naming Scheme

When using the GPS project wizard, you can select a number of predefined simple naming schemes which correspond to the default used by some Ada compilers. GPS will generate a package Naming in your project file corresponding to this scheme. You can also write such Naming manually.

For instance:

project My_Project is
   ...

   package Naming is
      for Spec_Suffix ("Ada") use ".1.ada";
      for Body_Suffix ("Ada") use ".2.ada";
      for Separate_Suffix use ".2.ada";
      for Dot_Replacement use ".";
   end Naming;
end My_Project;

or:

project My_Project is
   ...

   package Naming is
      for Spec_Suffix ("ada") use "_.ada";
      for Body_Suffix ("ada") use ".ada";
      for Separate_Suffix use ".ada";
      for Dot_Replacement use "__";
   end Naming;
end My_Project;

This approach applies only to projects where a single and consistent naming scheme is used for all source files. If multiple or inconsistent naming schemes are used, then you will need to follow Arbitrary Naming Scheme instead.

2.2.4. Ada Language Version

By default CodePeer assumes sources are using the Ada 2012 language (latest standard). If your sources are using an older version of Ada, then you will need to add the following to your project file:

package CodePeer is
   for Switches use ("-gnat95");
end Builder;

The switches corresponding to the various Ada versions are: -gnat83, -gnat95, -gnat2005, -gnat2012.

Note that some Ada 95 compilers support the overriding keyword but no other Ada 2005 features. In order to analyze such code, you need to add the -gnatd.D switch in your project file, in addition to the -gnat95 switch:

package CodePeer is
   for Switches use ("-gnat95", "-gnatd.D");
end CodePeer;

2.2.5. 32bits Mode

By default CodePeer assumes that the compilation target is the same as the host on which it is run. This is often a sufficient default, suitable for most 32 and 64bits Ada compilers, although one typical case where this is not sufficient is when using CodePeer in 64bits mode, and analyzing code designed for 32bits architectures. In this case, you can run CodePeer with the -32bits switch so that CodePeer will analyze the code assuming the same architecture, but in 32bits mode instead of 64bits. You can use this switch either from the command line, or specify it in your project file:

package CodePeer is
   for Switches use ("-32bits");
end CodePeer;

See also Target Configuration File for advanced configuration of the target.

2.2.6. Representation Clauses

If CodePeer generates errors during the SCIL generation related to Ada representation clauses, a simple way to address these errors is to add the -gnatI compiler switch to your project file:

package CodePeer is
   for Switches use ("-gnatI");
end CodePeer;

-gnatI instructs CodePeer to ignore representation clauses, as if they had been stripped from the source code.

2.2.7. Use of Predefined Ada Packages

The predefined Ada packages (in particular, children of Ada, System, and Interfaces) come packaged with CodePeer, so you do not need and should not include in your project file alternative predefined Ada source packages, such as are provided by some Ada compilers, since these predefined packages may contain nonportable constructs that CodePeer may not recognize.

For compiler specific packages, see Use of Compiler Specific Packages for accessing some of these. If this isn’t sufficient, you will need to include at least the package specs from your target compiler as part of your project file as for any other source file.

2.2.8. Use of Compiler Specific Packages

If your Ada code base is making use of compiler specific packages, CodePeer provides some of these packages preinstalled under install/share/gpr and accessible as preconfigured project files.

In particular you will find the following project files:

  • aa.gpr: ApexAda specific packages.
  • am.gpr: AdaMulti and AdaMagic specific packages.
  • oa.gpr: ObjectAda specific packages.
  • vads.gpr: VADS specific packages.
  • xgc.gpr: XGC specific packages.

To use these project files, add for example the following line to your project file (adjust the name of the file as needed):

with "am";

project My_Project is
   --  other declarations...
end My_Project;

If some compiler specific packages are missing, do not hesitate to contact your CodePeer support.

2.2.9. Project Attributes

In addition to the project attributes described in the GNAT User’s Guide and mentioned earlier in this chapter (e.g. Source_Dirs, Naming and IDE packages, ...), the following optional project attributes are available in the CodePeer package:

  • Additional_Patterns

    Extra MessagePatterns.xml file to use in addition to the default patterns file. this can be either a path relative to the project’s directory, or an absolute path.

  • CWE

    Enables displaying of relevant CWEs for messages in GPS and in text/CSV output (not in HTML reports). Possible values are “true” or “false”, e.g.:

    package CodePeer is
       for CWE use "true";
    end CodePeer;
    
  • Database_Directory

    CodePeer database directory to use for this project. By default, the database directory is codepeer/<project>.db. If you specify a relative directory, this directory is relative to the location of the project file itself.

  • Excluded_Source_Files

    List of project source file (as base names) which should be excluded from CodePeer’s analysis.

  • Message_Patterns

    Alternate MessagePatterns.xml file to use for this project.

  • Output_Directory

    CodePeer output directory to use for this project. By default, the output directory is codepeer/<project>.output. If you specify a relative directory, this directory is relative to the location of the project file itself.

  • Switches

    List of additional switches always used for this project.

Here is an example of a project file using some of these attributes:

project Prj1 is
   ...

   package CodePeer is
      for Excluded_Source_Files use ("file1.ads", "file2.adb");
      for Output_Directory use "project1.output";
      for Database_Directory use "/work/project1.db";
      for Switches use ("-level", "2");
      for Additional_Patterns use "ExtraMessagePatterns.xml";
      for CWE use "true";
   end CodePeer;
end Prj1;

2.2.10. Project File Example

Here is a complete example of a project file containing two directories with Ada 95 source files using an alternate naming scheme, to be used without GNAT and ignoring the representation clauses:

project My_Project is
   for Target use "codepeer";

   for Source_Dirs use ("sources/src1", "sources/src2");

   package CodePeer is
      for Switches use ("-gnat95", "-level", "2");
   end CodePeer;

   package Naming is
      for Spec_Suffix ("Ada") use ".1.ada";
      for Body_Suffix ("Ada") use ".2.ada";
      for Separate_Suffix use ".2.ada";
      for Dot_Replacement use ".";
   end Naming;
end My_Project;

2.3. Advanced Project File Set Up

When configuring CodePeer to analyze Ada code that has not been used with GNAT before, it is often necessary to follow some of the advices listed in this section.

2.3.1. Arbitrary Naming Scheme

If you are using a more complex naming scheme (e.g. files with mixed casing, no automatic mapping between unit names and file names, use of multiple units in a single file, etc...) then you have three options:

  • Use the File ‣ Project ‣ Add Complex File Naming Conventions... menu in GPS and follow the dialog. This will call the underlying command line tool codepeer-gnatname and modify the project file for you. See the GPS documentation for more details.

  • Use the codepeer-gnatname tool to generate the custom naming scheme automatically

    To create complex project files automatically from an existing directory structure, you can use the codepeer-gnatname utility from the command line. Here is a typical usage of codepeer-gnatname:

    codepeer-gnatname -Pmy_project "-d./**" "*.ad?" "*.spc" "*.bdy"
    

    which will create (or update) a project file called my_project.gpr listing all the Ada source files found under the current directory and all its subdirectories whose name follow the given patterns (all files ending with .ad<any character>, all files ending with .spc and all files ending with .bdy).

    Note that codepeer-gnatname requires a writable temporary directory. If the project file generated is empty, you might need to set the environment variable TMPDIR to a writable directory.

    See the gnatname documentation in the GNAT User’s Guide for more details on how to use gnatname.

  • Use the codepeer-gnatchop tool

    Alternatively, you can preprocess your sources to generate .ads/.adb files by running codepeer-gnatchop on all your Ada sources and use a simple project file on the generated sources, for instance under Linux:

    cd <root source directory>
    mkdir sources
    find . -name sources -prune -o -name '*.ad?' -exec codepeer-gnatchop {} sources \;
    

    This command will take all files ending with .ad<any character> under the current source tree, and generate a corresponding .ads/.adb file under a new directory called sources. You can then use in your project file:

    for Source_Dirs use ("sources");
    

2.3.2. Target Configuration File

Usually, using either the default settings, the -32bits or the -gnatI switch is sufficient to analyze code for most targets.

If you need to configure CodePeer so that it has a deeper knowledge and understanding of the target compiler, and in particular setting target dependent values such as endianness or sizes and alignments of standard types, then you might need to add the following to your project file:

package CodePeer is
   for Switches use ("-gnateT=" & project'Project_Dir & "/target.atp");
end CodePeer;

where target.atp is a file stored here in the same directory as the project file my_project.gpr, which contains the target parametrization. This file can be generated by calling the GNAT compiler for your target with the switch -gnatet=target.atp. The format of this file is described in the GNAT User’s Guide as part of the -gnateT switch description.

Here is an example of a configuration file for a bare board PowerPC 750 processor configured as big-endian:

Bits_BE                       1
Bits_Per_Unit                 8
Bits_Per_Word                32
Bytes_BE                      1
Char_Size                     8
Double_Float_Alignment        0
Double_Scalar_Alignment       0
Double_Size                  64
Float_Size                   32
Float_Words_BE                1
Int_Size                     32
Long_Double_Size             64
Long_Long_Size               64
Long_Size                    32
Maximum_Alignment            16
Max_Unaligned_Field          64
Pointer_Size                 32
Short_Enums                   0
Short_Size                   16
Strict_Alignment              1
System_Allocator_Alignment    8
Wchar_T_Size                 32
Words_BE                      1

float          6  I  32  32
double        15  I  64  64
long double   15  I  64  64

If your target compiler is not GNAT, or an old version of GNAT, then you can also build and run the small utility called generate_target which can be found under <codepeer install>/share/codepeer/target. See comments inside this file for instructions on how to use it.

Note that, depending on the Ada constructs you are using and the values specified in the target configuration file, some combinations will not be properly supported and will lead to errors during SCIL generation. In this case, consider using instead the -gnatI switch, or contact your CodePeer support for alternatives.

2.3.3. Using the GNAT Target Runtime Directory

If you are using GNAT as your target compiler and explicitly specify a runtime and target to use in your project, for instance:

for Target use "arm-eabi";
for Runtime ("Ada") use "ravenscar-sfp-stm32f4";

CodePeer will take such setting into account and will use the GNAT runtime directory, as long as your target compiler is found in your PATH environment variable. Note that you will need to use a matching version of GNAT and CodePeer (e.g. GNAT 18.2 and CodePeer 18.2).

The handling of runtimes of CodePeer is in fact unified with that of the GNAT compiler. For details, see “GNAT User’s Guide Supplement for Cross Platforms”, Section 3. If you specify a target, note that CodePeer may use additional configuration, see the section Target Configuration File.

If for some reason you do not have access to the GNAT compiler on the same machine as CodePeer (e.g. the GNAT cross compiler is installed on a different host than CodePeer) you will first need to copy the GNAT runtime directory in the CodePeer installation, under codepeer-prefix/libexec/codepeer/lib/gnat/.

For example, assuming you want to use a runtime called ravenscar-sfp-stm32f4, then first locate this runtime on the machine with the GNAT installation, e.g.:

arm-eabi-gnatls -v --RTS=ravenscar-sfp-stm32f4 | grep adalib

This command gives the path to <ravenscar-sfp-stm32f4 runtime>/adalib.

You then need to copy/transfer the <ravenscar-sfp-stm32f4 runtime> directory to the CodePeer installation, under codepeer-prefix/libexec/codepeer/lib/gnat/, for example using bash syntax:

scp -pr $(dirname $(arm-eabi-gnatls -v --RTS=ravenscar-sfp-stm32f4 | grep adalib)) \
  codepeer-machine:<codepeer-prefix>/libexec/codepeer/lib/gnat

2.3.4. Configuration of System Package (system.ads)

Some Ada compilers provide additional, nonportable definitions in the predefined package System which might lead to errors when CodePeer generates SCIL.

A solution to address this issue automatically is to use the pragma Extend_System in a pragma configuration file, either using one of the predefined GNAT extensions (e.g. Aux_Dec for the DEC Ada compiler or VADS for the VADS compiler, available via the project file vads.gpr as described in Use of Compiler Specific Packages), or by providing a customized s-auxcom.ads file.

For example, you can create a file called e.g. codepeer.adc located under the same directory where your project file is, which will contain:

pragma Extend_System (Aux_Dec);

or alternatively:

pragma Extend_System (Aux_VADS);

And configure your project file to take this file into account:

package Builder is
   for Global_Configuration_Pragmas use "codepeer.adc";
end Builder;

or if using Aux_VADS:

with "vads";
project My_Project is

   package Builder is
      for Global_Configuration_Pragmas use "codepeer.adc";
   end Builder;

end My_Project;

Similarly, if your target compiler provides additional definitions, you can manually create a s-auxcom.ads file containing these additional definitions, e.g.:

package System.Aux_Compiler is
   pragma Preelaborate;

   function To_Integer (Addr : Address) return Integer;
   function To_Address (Int  : Integer) return Address;

   No_Addr      : constant Address := Null_Address;
   Address_Zero : constant Address := Null_Address;

   Assertion_Error : exception;

   ...
end System.Aux_Compiler;

and then specify:

pragma Extend_System (Aux_Compiler);

in codepeer.adc.

See the GNAT Reference Manual for more details on Pragma Extend_System.

Also note that you should never include the compiler System package in your project file (either in your source file list or even in your source directories), as CodePeer needs to use its own provided system.ads.

2.3.5. Using Preprocessing

In order to enable the GNAT integrated preprocessor, you can use the -gnateD and -gnatep switches, e.g.:

package CodePeer is
   for Switches use ("-gnateDVAR1=xxx", "-gnateDVAR2=yyy");
end CodePeer;

See section Integrated Preprocessing in the GNAT User’s Guide for more details. See also the section Form of Input Text for gnatprep in chapter Preprocessing with gnatprep for more details on the syntax supported by the GNAT preprocessor.

2.3.6. Ignoring Pragmas

In some cases, nonportable pragmas are used across Ada technologies in an incompatible way, generating some spurious error messages when CodePeer analyzes these files. In order to address these issues, you can configure your project file to ignore a set of pragmas via the Ignore_Pragma pragma that you should place in a codepeer.adc file as explained in Configuration of System Package (system.ads). For example, if you want to ignore pragmas called Import_Procedure and Import_Function you can put in your codepeer.adc:

pragma Ignore_Pragma (Import_Procedure);
pragma Ignore_Pragma (Import_Function);

Similarly if you want to ignore pragma Global:

pragma Ignore_Pragma (Global);

If not already done, you need configure your project file to take this file into account:

package Builder is
   for Global_Configuration_Pragmas use "codepeer.adc";
end Builder;

2.3.7. Providing Stubs for Missing Generic Bodies

CodePeer will ignore missing bodies and will make reasonable presumptions about calls to such unknown subprograms (see CodePeer Presumptions).

However it will generate an error when it encounters a generic package whose body is missing at instantiation time. In order to work around this error, you can provide a skeleton for the generic package via the codepeer-gnatstub utility, e.g.:

codepeer-gnatstub -Pmy_project generic_package.ads

will generate a file generic_package.adb which can be used by CodePeer.

2.3.8. Detection of Floating Point Overflow

CodePeer assumes that floating point operations are carried out in single precision (binary32) or double precision (binary64) as defined in the IEEE-754 standard for floating point arithmetic. You should make sure that this is the case on your platform. For example, on x86 platforms, by default some intermediate computations may be carried out in extended precision, leading to unexpected results. With GNAT, you can specify the use of SSE arithmetic by using the compilation switches “-msse2 -mfpmath=sse” which cause all arithmetic to be done using the SSE instruction set which only provides 32-bit and 64-bit IEEE types, and does not provide extended precision. SSE arithmetic is also more efficient. Note that the ABI allows free mixing of units using the two types of floating-point, so it is not necessary to force all units in a program to use SSE arithmetic.

CodePeer considers the floating point values which represent positive, negative infinity or NaN as invalid, and it checks that such values cannot occur.

By default, CodePeer will only detect potential overflows on floating point operations on constrained floating point types (user floating point types with explicit ranges) and not on unconstrained types (e.g. predefined float types) unless you specify -level max where overflows are checked on all float types.

You can also ask CodePeer to check for possible floating point overflows on unconstrained types at any level (which will then lead to infinite values) via the -gnateF compiler switch, e.g.:

package CodePeer is
   for Switches use ("-gnateF");
end CodePeer;

2.3.9. CodePeer Specific Project Settings

If you are using project files also to build with GNAT and need to use e.g. different builder switches between GNAT builds and CodePeer analysis, you can then use a scenario variable to differentiate the two modes in your project file:

type Build_Type is ("Debug", "Production", "CodePeer");
Build : Build_Type := External ("Build", "Debug");

package Builder is
   case Build is
      when "CodePeer" =>
         for Global_Compilation_Switches ("Ada") use ("-gnatI");
         -- -gnatI is only relevant for CodePeer
      when others =>
         for Global_Compilation_Switches ("Ada") use ("-O", "-g");
         -- Switches only relevant when building
   end case;
end Builder;

and run codepeer with the -XBuild=CodePeer switch.

2.3.10. Ignoring Source File Timestamp Mismatch

If your environment changes the timestamps of your source files between CodePeer runs (without changing the source file contents), then in order to minimize the regeneration of SCIL files you can specify the -m switch in the Builder package of your project file, so that checksums rather than timestamps should be used for determining whether source files have changed since the previous run:

package Builder is
   for Switches ("Ada") use ("-m");
end Builder;

2.3.11. Ignoring Exception Handlers

By default CodePeer tries to take exception handlers into account in its analysis, although by doing so this can lead to a loss of precision in the detection of possible (or certain) run-time errors. If you want CodePeer to analyze the code by completely ignoring exception handlers (behave as if the exception handlers were stripped from the code) then you can add the -gnatd.x switch, e.g.:

package CodePeer is
   for Switches use ("-gnatd.x");
end CodePeer;

2.3.12. Handling Enumeration Representation Clauses

Even without -gnatI, CodePeer by default ignores enumeration representation clauses, to reduce the various implicit representation transformations required by such clauses, which can produce confusing output. If your application uses Enum_Rep, Enum_Val, or Unchecked_Conversion to manipulate the underlying codes specified by an enumeration representation clause, then you may want to override this CodePeer default by using the compiler switch -gnatd.I. This will cause CodePeer to obey the enumeration representation clause and ensure that Enum_Rep, Enum_Val, and Unchecked_Conversion are interpreted correctly for this enumeration type. This switch can be added to your project file, as follows:

package CodePeer is
   for Switches use ("-gnatd.I");
end CodePeer;

2.4. Running CodePeer

This section describes how to run CodePeer from the command line (for simple experiments or for running jobs automatically), as well as how to use CodePeer from the GNAT Programming Studio and GNATbench (Eclipse plug-in).

2.4.1. Running CodePeer from the Command Line

In order to run a code review with CodePeer from the command line, you need to perform the following steps:

  • Run codepeer

    See Command Line Invocation for more details. A typical invocation of codepeer will look like:

    $ codepeer -Pmy_project
    

    Note that if you want to run codepeer as part of a script, you should consider using also the -quiet switch.

    This command will first run codepeer-gprbuild to generate or update SCIL files (intermediate representation), and then will run the CodePeer main engine.

    This will update the CodePeer database under codepeer/my_project.db. You can then view the results using GPS, a Web browser, or from the command line, for example:

    $ codepeer -Pmy_project -output-msg-only
    alias.adb:10:11: high: divide by zero fails here: requires Page_Size /= 0
    

    Note that if you want to systematically generate messages from the command line, you can then use directly:

    $ codepeer -Pmy_project -output-msg
    alias.adb:10:11: high: divide by zero fails here: requires Page_Size /= 0
    

    See How to View CodePeer Output for more details.

    In addition, the codepeer switch -level can be used, based on the kind of analysis needed, and the size of the source code analyzed, see CodePeer Levels for more details.

2.4.2. Running CodePeer from GPS

When CodePeer is installed and found on your PATH, GPS will detect it automatically and provide a new CodePeer top level menu with the following contents.

The main entry point to run CodePeer and display a code review is the Analyze All menu.

  • Analyze All

    Generate SCIL for sources of the whole project tree if needed, then run CodePeer, displaying a progress bar giving an estimate of the review state, and then load the CodePeer report window. See Viewing CodePeer Output in GPS for more details on the report window. An HTML report is also generated, available via the Display HTML Report menu. This menu item will use the CodePeer switches set in your project files, if any. By default, CodePeer annotations such as automatically generated contracts will be imported and displayed in the source editor. Note that this can take a significant amount of time for large projects and can be disabled via the GPS Preferences.

  • Analyze...

    _images/codepeer-analyze.jpg

    Open a dialog where you can select more precisely the kind of analysis performed and in particular to add or override CodePeer switches defined in your project file. You can specify any command line switch in the bottom text input, as listed in Command Line Invocation. In addition you can also select graphically some of these options:

    • Analysis level

      Allows specifying the precision of analysis and corresponding time and memory. Maps to the -level switch.

    • Messages

      Specify the verbosity and number of messages produced by CodePeer. Maps to the -messages switch. The default is -messages normal unless specified otherwise in your project file.

    • Baseline run

      Sets the run as the baseline for future comparisons. Maps to the -baseline switch.

    • No race condition

      Disable global race condition analysis. Maps to the -no-race-conditions switch.

    • Root project only

      CodePeer will only analyze the source files associated with the root project file (presuming your application uses a tree of project files to represent all of its constituents). Maps to the --no-subprojects switch.

    • Force analysis

      Force generation of all SCIL files and analysis of all files. Maps to the -f switch.

    • GNATcheck

      Launch GNATcheck and collect its messages, see GNATcheck Integration.

    • Cutoff

      Specify the reference (cut off) run to perform a comparison of messages. Maps to the -cutoff switch, see also CodePeer Baselines.

    • Baseline review #

      Change the default baseline. Maps to the -set-baseline-id <id> switch.

    • Multiprocessing

      Specify the number of processes to generate SCIL files and analyze files. Maps to the -j switch.

    Once the selection is done, click on the Execute button to get a behavior similar to Analyze All.

  • Analyze File

    Analyze the current source file only. This menu is available only when a source file is selected in GPS. Note that the analysis is performed without taking into account effects of calls outside the selected file, and the results of this run are not entered into the CodePeer historical database. In addition, the messages are displayed in the Locations view only, without opening the CodePeer report view. See Running CodePeer in Compiler Mode for more details on this capability. Note that analyzing a subunit (separate unit) or a generic unit will have no effect: in the case of subunits you need to analyze the enclosing unit, and analyze instantiations of generics to get messages on generic units.

    If you would like to get a CodePeer report view, even when analyzing only a single file, then you can use Analyze... instead, and append %F to the end of the command line, which requests an analysis of the current file only.

  • Analyze File by File...

    _images/codepeer-file-by-file.jpg

    Similar to Analyze File for all files of the project. Analysis is performed incrementally, so only files that have changed since the last run will be reanalyzed and messages produced. See Running CodePeer in Compiler Mode for more details on this capability. Similarly to Analyze..., you can specify relevant custom switches either manually via the text input at the bottom of the dialog, or via the graphical interface for some of the switches:

    • Messages

      Specify the verbosity and number of messages produced by CodePeer. Maps to the -messages switch. The default in compiler mode is -messages min unless specified otherwise in your project file.

    • Multiprocessing

      Specify the number of processes to generate SCIL files and analyze files. Maps to the -j switch.

    • Root project only

      CodePeer will only analyze the source files associated with the root project file (presuming your application uses a tree of project files to represent all of its constituents). Maps to the --no-subprojects switch.

    • Force analysis

      Force generation of all SCIL files and analysis of all files. Maps to the -f switch.

  • Display Code Review

    Assuming CodePeer has already been run previously, GPS will load the CodePeer review information from the database and display a summary of the review. See Viewing CodePeer Output in GPS for more details.

  • Display HTML Report

    Open a default browser on CodePeer’s HTML report, assuming CodePeer was run previously (via e.g. Analyze All). See HTML Output for more information.

  • Generate CSV Report...

    Generate a CodePeer report in CSV format, and open the report in a source editor. This menu will open an intermediate dialog where you can specify extra switches to generate the CSV report, in particular if you want to use the -security switch (see Text Output and CSV Output for more details).

  • Advanced

    This submenu provides advanced capabilities, less often needed:

    • Regenerate Report...

      Run CodePeer to only regenerate reports by reading the database. Maps to the -output-msg-only switch. This might be useful for e.g. changing the baseline or cutoff point of comparison, or for generating an HTML report.

    • Generate SCIL...

      Note: the Analyze All and Analyze... menus generate SCIL files automatically, so this menu is not needed in general. Open a dialog to generate SCIL for your project. The default switches should in general be sufficient, in which case, pressing enter or clicking on the Execute button will launch the SCIL generation. Alternatively, you might need to add some extra switches for better SCIL generation, depending on your sources.

    • CodePeer Log

      Open a text editor with the low level log file produced by CodePeer. This can be useful for example to understand why CodePeer did not generate the expected output, or to send CodePeer bug reports.

    • Remove Lock

      Remove the lock associated with a CodePeer run. In normal conditions, CodePeer will handle locks automatically. In case of an unexpected exit during CodePeer execution, a lock file may be left behind, which can be removed using this menu. This menu should not be used while CodePeer is still running.

    • Remove XML Code Review

      GPS generates an intermediate XML file containing the contents of the last code review as stored in the CodePeer database. In normal mode of operation, GPS will generate this file when needed. This menu can be used to manually remove this xml and force GPS to regenerate it the next time e.g. the Display Code Review menu is used.

    • Remove SCIL

      Remove all SCIL directories associated with the project. This can be useful when e.g. upgrading to a new version of CodePeer or when you want to start a clean analysis from scratch.

    • Remove SCIL & DB

      Same as above, and in addition, also removes the CodePeer historical database and any other CodePeer artefacts.

Note that most of the menus will launch commands that can be configured or tuned using the Edit ‣ Preferences menu, in the Build Targets section. See the GPS documentation for more details on the build targets.

GPS allows sharing the database among several users. Paths to database and output directories can be defined using the project properties editor (Edit ‣ Project Properties...). See Project Attributes.

In addition, new preferences specific to CodePeer are also defined, see GPS Preferences for more details.

2.4.3. Running CodePeer from GNATbench

When CodePeer is installed and found on your PATH, GNATbench will detect it automatically and provide a context sensitive menu when you right click on the project. The context menu will have a Codepeer entry with the following submenus:

  • Analyze All
  • Analyze...
  • Analyze File
  • Analyze File By File
  • Run CodePeer
  • Regenerate Report
  • Clear CodePeer Markers
  • Redisplay CodePeer Markers
  • Display HTML Report
  • View Race Condition
  • Generate SCIL

The main entry point to run CodePeer and display a code review is the Analyze All menu.

  • Analyze All

    Right click on the Project and then click the Codepeer ‣ Analyze All menu. Analyze All generates SCIL for sources of the whole project tree if needed and run CodePeer. When CodePeer starts running, a Console window will come up in the bottom pane; this window will contain any errors or informational messages generated by CodePeer while it is running. At the end of the analysis, the CodePeer Problem Details tab will be highlighted and the messages can be seen in the bottom pane under the CodePeer messages heading. See Viewing CodePeer Output in GNATbench for more details on the report window. You can view the HTML report by clicking the Display HTML Report menu.

  • Analyze...

    Open a dialog where you can select more precisely the kind of analysis performed. In particular you can select to analyze the root project only, and you can change the analysis level. Once the selection is done, click on the Execute button to get a behavior similar to Analyze All. In order to perform a quick analysis, set the Analysis level to 0 or 1. In order to analyze only the root project, enable the Analyze root project check box.

  • Analyze File

    Analyze the current source file only. This menu is available only when a source file is selected in GB. Note that the analysis is performed without taking into account effects of calls outside the selected file, and the run is not taken into account in the CodePeer historical database. See Running CodePeer in Compiler Mode for more details on this capability.

  • Analyze File by File...

    Similar to Analyze File for all files of the project. Analysis is performed incrementally, so only files that have changed since the last run will be reanalyzed and messages produced. See Running CodePeer in Compiler Mode for more details regarding this.

  • Run CodePeer

    Right click on the Project and select the Codepeer->Run CodePeer menu. The Run CodePeer dialog will pop up. The default switches should be sufficient for running. You can choose extra switches if needed. See Command Line Invocation for more details on CodePeer switches.

    _images/codepeer-run-gb.jpg

    Click ‘Proceed’ button to start the analysis. You will see some messages from the CodePeer run in the Console tab. At the end of the run, the CodePeer Problem Details tab will be highlighted and the messages can be seen in the bottom pane under CodePeer Messages. Click on an arrow for a file to expand the messages for that file.

  • Regenerate Report

    Right click on the Project and then select CodePeer-> Regenerate Report menu to regenerate reports by reading the database. A dialog box will appear containing various switches. This might be useful for e.g. changing the baseline or cutoff point of comparison, or filtering messages to generate HTML report. Once you select the switches, then you can press Proceed to regenerate reports without running another analysis of the sources.

  • Clear CodePeer Markers

    Right click on the Project and then select Clear CodePeer Markers menu. It will remove all the CodePeer markers both annotation and problem markers from the editor window area.

  • Redisplay CodePeer Markers

    Right click on the Project and then select Redisplay CodePeer Markers menu. It will recreate all the CodePeer markers that have been cleared for this project without running the CodePeer. It is assumed that CodePeer has been run before for this project.

  • Display HTML Report

    Right click on the Project and then select Display HTML Report menu. It will open a default browser on CodePeer’s HTML report, assuming CodePeer was run previously (via e.g. Analyze All menu). See HTML Output for more information.

  • View Race Condition

    Right click on the Project and then select Codepeer->View Race Condition menu. It will open a new view titled “Race Condition Details” in the bottom pane. In this view you can see results associated with race condition analysis.

  • Generate SCIL

    Note: the Analyze All menu generates SCIL files automatically, so this menu is not needed in general. Right click on the Project and then select the Codepeer->Generate SCIL menu which will open a dialog. Select this menu to generate SCIL files for your project. The default switches should be sufficient in general. If needed, you can select extra switches for better SCIL generation (e.g. -gnatI). At the end, press enter or Proceed button to generate SCIL files.

2.4.4. Running CodePeer from Jenkins

Install <install_dir>/share/jenkins/plugins/codepeer*.hpi into your Jenkins installation. See the Jenkins documentation for more information.

When the jenkins-codepeer-plugin is loaded in your Jenkins instance, it will automatically register a new Build Step available from the project configuration view.

The global configuration will have a CodePeer entry with the following setting:

  • CodePeer executable

The per-project configuration will have a CodePeer Build Step with the following regular settings:

  • Project file
  • Working directory
  • GPR_PROJECT_PATH
  • Analysis level

And the following Advanced settings:

  • Messages verbosity level
  • Jobs count
  • CodePeer executable
  • Ignore exit code
  • Additional CodePeer options

Access the global configuration by navigating from the main dashboard to Manage Jenkins ‣ Configure System, section CodePeer Analyser.

  • CodePeer executable

    Location of the CodePeer executable to use at the system level. Leave empty to use the default CodePeer located in PATH. This setting is overridden by the equivalent per-project setting (see the per-project CodePeer Executable setting).

Access the per-project configuration by navigating from the main dashboard to <your-project> ‣ Configure.

Create a new “build step” by selecting Add build step ‣ Analyse with CodePeer.

  • Project file

    Path to the project file to run the analysis on. Relative to Jenkins workspace directory (e.g. the root of the repository).

  • Working directory

    The directory from where to execute CodePeer, also relative to Jenkins workspace directory. If left empty, the workspace directory is used.

  • GPR_PROJECT_PATH

    Overrides the environment variable GPR_PROJECT_PATH used during CodePeer execution. The original value can be extended, e.g.:

    /gpr/project/path:$GPR_PROJECT_PATH
    
  • Analysis level

    The level of analysis to be performed. This is equivalent to using -level on the command line.

  • Messages verbosity level (Advanced Options)

    The level of verbosity for generated messages. This is equivalent to using –messages on the command line.

  • Jobs count (Advanced Options)

    The number of simultaneous processes launched during an analysis. This is equivalent to using -j on the command line.

  • CodePeer executable (Advanced Options)

    Location of the CodePeer executable to use, defined at the project level. Overrides the global setting of the same name.

  • Ignore exit code (Advanced Options)

    Any exit code from CodePeer other than 0 is treated as an error and the build will fail. Enable this option to ignore the exit code.

  • Additional CodePeer options (Advanced Options)

    This plugin does not expose all CodePeer options. Use this setting to configure any additional option to add to the command line.

2.5. Running CodePeer Faster

In some cases, it can be useful to get feedback quickly from CodePeer, possibly at the expense of less precise results (e.g. when running CodePeer manually after each set of change, as opposed to running CodePeer nightly automatically).

2.5.1. Relevant Switches

CodePeer provides several switches which, separately or combined, will provide a much quicker analysis. The most relevant switches are:

-j<number of cores> E.g. -j0 on an 8-core machine, which will launch 8 CodePeer analyses in parallel instead of 1.
-level min Analyze subprograms one by one. Similar to compiler warnings.
-no-html-output Disable generation of HTML reports. On large sources, generation of HTML can take a long time, so if you do not need the HTML output, you can disable it via this switch.
-method-timeout <seconds> E.g. -method-timeout 20, which helps avoid CodePeer spending too much time on a single, complex subprogram, and instead causes it to be skipped. Note that -level 0/1/2 sets this value by default to respectively 10/20/30. At levels 3 and 4 the default is 600 (10 minutes).
-compiler-mode Run in compiler mode, which provides local analysis similar to -level 1, and incremental analysis, without support for history and with text output only, see Running CodePeer in Compiler Mode for more details.

In other words, running with:

codepeer -j0 -level min -no-html-output

on a multicore machine will divide by a significant factor the CodePeer execution time.

Similarly, running with:

codepeer -j0 -compiler-mode

will also significantly reduce analysis and reanalysis time, with the limitations of the compiler mode described in Running CodePeer in Compiler Mode.

Note that the -j switch will be taken into account by the following processes:

  • SCIL generation (codepeer-gprbuild)
  • codepeer_be (partition analysis)

Some processes (e.g. db_lister, codepeer_msg_reader, codepeer_bridge) will ignore the -j switch.

2.5.2. Disabling Analysis of Subprograms or Files

Another option is to selectively disable CodePeer’s analysis of a particular subprogram or set of subprograms or files, as described in Partial Analysis.

2.6. Running CodePeer in Compiler Mode

An alternate way to run CodePeer is to use the -compiler-mode switch, where CodePeer will behave more like a compiler by analyzing files one by one, and only reanalyzing files which have changed since the last run. For example:

$ codepeer -compiler-mode -j0 -Pmy_project

Will analyze all files in my_project and generate messages in the standard output for each file analyzed.

You can also access this capability from GPS via the menu CodePeer ‣ Analyze File by File..., see Analyze File by File.

Most CodePeer switches are relevant in this mode, in particular:

  • -file
  • -j
  • –no-subprojects
  • -U

CodePeer switches from the command line and from the project file are taken into account, whenever relevant.

In addition, the -m switch for the builder can be relevant, as described in Ignoring Source File Timestamp Mismatch.

Compiler mode has some advantages:

  • Provides incremental analysis by taking advantage of gprbuild’s ability to only recompile/reanalyze files that have been modified since the last run. Note that messages from unchanged files analyzed from the previous run are also displayed.
  • Each file is analyzed in parallel when using the -j switch
  • Uses less memory
  • Skips several extra phases done by CodePeer (generation of HTML files, text listings, update of the historical database).

As well as several limitations:

  • Analysis is limited per unit, so no global analysis is performed (roughly equivalent to -level 1)
  • No extra information is generated (no html, no historical database, no annotations), which means in particular less information available to understand messages
  • Limited integration in the IDEs (no CodePeer report window, no display of extra information such as backtraces or possible values of variables)
  • No history of previous runs is stored
  • The only way to review messages is via pragma Annotate

2.7. Reducing the Number of False Alarms

By default CodePeer will try to detect as many potential issues as possible, at the expense of generating false alarms. You can tell CodePeer to concentrate on detecting only the most likely errors and generate many fewer false alarms (also known as false positives) via the -messages min switch. Note that this switch is enabled by default already at -level 0, -level 1 and when using -compiler-mode.

2.8. CodePeer Levels

You can configure CodePeer to perform its analysis at different levels via the -level switch, to tune the accuracy of analysis needed and depending on the size of the source code analyzed.

-level sets the level of analysis, which impacts both time and accuracy. Note that messages for lower levels are not necessarily a subset of those for higher levels. The switch -messages can be used to filter messages that have a higher probability of being false positives, in particular via -messages min.

Level Description Recommended Code Characteristics
-level 0 or -level min Light and fast analysis similar to compiler warnings or linters. Each subprogram is analyzed independently. Enables -messages min -no-race-conditions. No code size or complexity limit.
-level 1 Similar to level 0, a bit slower. Extra analysis of nested subprograms and initialization procedures generated by the compiler. Enables -messages min -no-race-conditions. No code size or complexity limit.
-level 2 Analyze by small groups of units. Slower analysis, a bit more precise. Enables -no-race-conditions. No code size or complexity limit.
-level 3 Semi-global analysis. Units will be analyzed globally as much as possible, and an automatic partioning is performed to complete the analysis within the memory constraints of the machine. Suitable for less than 1 million SLOC and subprograms with a cyclomatic complexity below 40
-level 4 or -level max Global analysis. Analyze all units together with no partitioning. May require large amounts of memory and time. Recommended only for very accurate and complete analysis to detect all potential cases of run-time errors exhaustively at the expense of many false positives. Enables -no-presumptions -messages max -gnateF. Suitable for less than 200K SLOC and subprograms with a cyclomatic complexity below 20.

So typically -level 0/1 is recommended when analyzing large source code base initially, or to get results quickly. -level 3 is currently the default, and can be used for performing global analysis, on code base no larger than 1 million lines of code.

-level 4 is only suitable for small to medium code base (typically less than 200K lines of code) for a sound (messages reported with high rank are certain) and complete (all possible errors are reported) analysis, where a systematic review of all potential run-time checks is required (including reviewing many false positives) and where time of analysis is not important. In terms of memory requirements, a 64bits configuration with at least 1 GB of memory per 10K SLOC is required to perform analysis at level 4.

2.9. CodePeer Baselines

CodePeer maintains a historical database of all the analysis performed on a specific project and all of the associated messages. This database allows CodePeer to specify if a message is new, unchanged or removed. Instead of classifying the message by comparing the current analysis to the previous one, CodePeer uses a more elaborate notion of baseline run or simply baseline. A baseline is the run of reference against which the new analysis is compared to. Each analysis level has its baseline which is, by default, the first run performed at this level (CodePeer will not compare two runs performed at two different analysis levels).

The baseline stays the same from one run to another unless specified otherwise with either -baseline or -set-baseline-id <run_id> switches:

  • -baseline

    A run with the -baseline switch will keep the same baseline as the previous run but will become the new baseline for the following runs.

  • -set-baseline-id <run_id>

    Using -set-baseline-id <run_id> makes the run with the specified run_id the new baseline starting from the current run. For a specific level each run is given a unique id (a run with id 3 corresponds to the third analysis done at its analysis level). GPS displays the ids of the current run and its associated baseline (or cutoff if specified, see below) at the top of the “CodePeer report” tab (see here).

In addition, the user can temporarily ignore the baseline by setting a cutoff with the switch -cutoff <run_id>.

  • -cutoff <run_id>

    The current run is compared to the run with id run_id, without impacting the baseline.

All these switches can be used in combination with -output-msg-only.

  • -output-msg-only

    Adding -output-msg-only lets you display the current run messages without performing a new analysis. You can then compare the current run with any other runs (using -cutoff), or manipulate the baseline (using -baseline or -set-baseline-id) after the analysis is done. In GPS setting -output-msg-only corresponds to using the “Regenerate Report...” menu (in “Codepeer” -> “Advanced”).

In GPS you can set -baseline by checking the “Baseline run” box in either “Analyze...” menu or “Regenerate Report...” menu. In the same menus, you can set -set-baseline-id <run_id> with the “Baseline review #” option and -cutoff <run_id> with the “Cutoff” option (See Running CodePeer from GPS).

The typical workflow is to make successive runs until reaching a satisfactory state. At this point, run CodePeer with -output-only -baseline to set this run as the new baseline. Afterwards, you can always compare the current run with other runs with -output-only -cutoff <run_id>. If later on you find that the baseline is not satisfactory, set a specific one with -set-baseline-id <id>.

Note:By default the status of the messages are not displayed in the text output of CodePeer (as opposed to GPS and the html output where you can filter the messages with their status). In order to display the status of the messages in the text output you need to tell CodePeer to use the CSV format with the switch -csv. In this format CodePeer specifies if a message is new or unchanged, you can also print the removed messages with the switch -show-removed. Furthermore, you can compare two arbitrary runs by setting a cutoff and manually override the current run via the -current switch. See Text Output for a complete list of switches supported with -output-msg(-only).

2.10. External Tools Integration

CodePeer can launch external tools to collect their messages, report them and add them to its database. This is done in addition to CodePeer’s core analysis.

As for other messages, you can use the Message Patterns mechanism to filter the external messages (by their source and by their category). A default ranking is chosen for each category of external messages in the MessagePatterns.xml file. See Format of MessagePatterns.xml File for more details.

2.10.1. GNAT Warnings Integration

In order to tell CodePeer to collect the GNAT front-end warnings, the switch --gnat-warnings must be specified.

When specified, CodePeer calls the GNAT front-end with the warnings enabled by default by GNAT, and optionally specified as compiler switches in your project file (when using project files also for compilation). You can refine this default by specifying the -gnatw parameters explicitly as optional parameters to --gnat-warnings, as in:

$ codepeer -Pmy_project --gnat-warnings=a.u

These switches will be enabled in addition to the ones specified elsewhere in your project. If you want to cancel the effect of other switches, you can specify the letter A (which corresponds to the -gnatwA switch), e.g.:

$ codepeer -Pmy_project --gnat-warnings=Au

Note that:

  • You need to use pragma Warnings (Off) instead of pragma Annotate to review messages in the source code.
  • Project attributes in the CodePeer package (in particular Excluded_Source_Dirs and Excluded_Source_Files) are ignored when generating GNAT warnings. You need to use the corresponding project level attributes instead if needed.

2.10.2. GNATcheck Integration

In order to tell CodePeer to collect the GNATcheck messages, the switch --gnatcheck must be specified.

Note that GNATcheck requires a file that describes the rules that it should check. Such a file can be created with the help of GPS through the menu: Analyze ‣ Coding Standard ‣ Edit Rules File (see here for more details). Refer to the GNATcheck Reference Manual for the complete GNATcheck documentation.

2.11. Partial Analysis

This section describes how to perform a partial analysis, and in particular, how to exclude entities (projects, directories, files, packages, subprograms) from analysis.

2.11.1. Excluding Subprograms or Packages From Analysis

To selectively disable CodePeer’s analysis of a particular subprogram or set of subprograms, you can add in your Ada source code a pragma Annotate of the form:

pragma Annotate (CodePeer, Skip_Analysis);

When used in this way, an Annotate pragma takes exactly these two arguments. The pragma may be placed at the beginning (possibly preceded only by different Annotate pragmas) of the declaration list of a subprogram body, a package body, or package visible part. In the case of a subprogram body, CodePeer’s analysis of that subprogram body (and anything declared therein, including nested subprograms) will not be performed. In the case of a package body, CodePeer’s analysis of any subprogram body occurring (directly or indirectly) within the package body will not be performed; this includes any such subprogram bodies that are implicitly generated by the compiler (e.g., the compiler might choose to generate a default initialization subprogram for a type declaration). In the case of a package visible part, analysis of subprogram bodies occurring in the package specification (as well as the package body) will not be performed; note that a subprogram body can occur in a package specification as part of an instantiation of a generic unit. The subprogram or package in question may be a generic unit or may occur within a generic unit; in this case, the pragma will be replicated (as described in Ada RM 12.3(13)) when an instance of the generic unit is declared and will affect CodePeer’s analysis of the instance as described in this section.

When an Annotate pragma is used in this way to prevent CodePeer’s analysis of a subprogram body, the analysis of clients of the subprogram will be affected in the same way as if the body of the subprogram were unavailable for some other reason (e.g. a missing .adb file).

Note that an annotate pragma of this form is ignored by the compiler when generating code; it only affects CodePeer’s analysis.

Here is an example of usage to disable analysis of a specific subprogram:

procedure Complex_Subprogram (...) is
   pragma Annotate (CodePeer, Skip_Analysis);
begin
   ...
end Complex_Subprogram;

And similarly for a package:

package Complex_Package is
   pragma Annotate (CodePeer, Skip_Analysis);

   ...
end Complex_Package;

2.11.2. Excluding Files From Analysis

If you want to exclude some files from analysis (because e.g. CodePeer is taking lots of time analyzing them, and these files do not contain useful subprograms for CodePeer to analyze), you can use the Excluded_Source_Files project attribute in package CodePeer, for example:

package CodePeer is
   for Excluded_Source_Files use ("xxx.adb");
   -- Analysis of xxx.adb generates lots of timeouts, skip it for now
end CodePeer;

Note that you should always specify the basename of the excluded files, with no path information. The path information is computed automatically by CodePeer based on other project properties.

CodePeer will still generate SCIL for the excluded file, but it will not attempt to analyze it. If you want to also exclude files from SCIL generation and these files are not in the transitive closure of other files (e.g. a body file, as opposed to a spec file used by other Ada units), then you can use instead the project level Excluded_Source_Files attribute:

project My_Project is
   for Excluded_Source_Files use ("xxx.adb");
end My_Project;

2.11.3. Excluding Directories From Analysis

If you want to exclude from analysis all source files from a given set of directories, you can use the Excluded_Source_Dirs project attribute in package codePeer, for example:

package CodePeer is
   for Excluded_Source_Dirs use ("directory1", "directory2");
end CodePeer;

You can specify absolute directories or directories relative to the location of the project file (same as for source directories).

2.11.4. Excluding Projects From Analysis

If you have a tree of project files (.gpr) and want to exclude some entire projects (aka subsystems) from CodePeer analysis, you can do it by adding the following project attributes to each of the projects involved:

for Externally_Built use "True";

This attribute tells CodePeer to not build/generate SCIL files for this project, thus disabling analysis on all source files for this project.

Projects using files (e.g. spec) from this project will still be analyzed, as well as generic instantiations made in other projects.

2.12. Source Annotations

CodePeer’s analysis and reporting can be affected by adding certain pragmas to your source code. In particular, pragma Annotate can be applied in a few different ways:

  • pragma Annotate (CodePeer, False_Positive|Intentional, “<check name>”, “<review message>”);

    This form can be used to suppress messages by classifying them as false positives or as intentional errors. See the section on reviewing messages Through Pragma Annotate in Source Code. Note that there’s an example of use given in Add message review pragmas.

  • pragma Annotate (CodePeer, Skip_Analysis);

    Pragma Annotate can also be used to skip the analysis of specific subprograms or packages, as described in Partial Analysis.

  • pragma Annotate (CodePeer, Single_Thread_Entry_Point|Multiple_Thread_Entry_Point, “entry point”);

    Pragma Annotate can be used to aid in identifying race conditions, as discussed in Identify Possible Race Conditions.

  • pragma Annotate (CodePeer, Mutex, “lock subprogram”, “unlock subprogram”);

    Also used to Identify Possible Race Conditions.

In addition, the contract-related pragmas Assert, Assume, Precondition, and Postcondition can be added in the source code, serving as manual checks that can aid or enhance CodePeer’s analysis, as documented in the section on User Checks. Also see the section Improve your code specification for an example of using pragma Precondition to enhance error detection.