Short introduction to CPAchecker

CPAchecker is a tool for configurable software verification of C programs.

Requirements

  • At least Java 8 (e.g. Oracle JRE, OpenJDK)
  • The CPAchecker project directory. Therefore download and extract the content of the CPAchecker tar or zip file into a directory of your choice.
  • Any source code file, which should be checked by CPAchecker. All programs need to pre-processed with the C pre-processor.

For the installation of CPAchecker see Installation.

First run

You can execute CPAchecker with the following command. The current directory should be the extracted CPAchecker project directory.

    scripts/cpa{.sh|.bat} [ -config <CONFIG_FILE> ] [ -spec <SPEC_FILE> ] <SOURCE_FILE>
  • -config: Configuration file to enable certain analyses like predicate analysis.
  • -spec: Specification file, which searches for certain labels and assertions in the source code.

Either a configuration file or a specification file needs to be given.

Result

When CPAchecker terminates, it generates a report in form of a HTML document in addition to the console output. The report file normally resides in the output folder inside the CPAchecker directory. The name depends on the result of the analysis.

  • If the program was proven to be correct, the file will presumably be named Report.html.
  • If the analysis found a counterexample, the report file is normally called Counterexample.x.html, where x is a number corresponding to the x-th counterexample that was found. The exact name of the report (in case one was created) is also stated at the end of CPAcheckers command-line output:

The generated HTML document contains the following tabs:

  • CFA tab: shows the control-flow automaton of the program. You can also just view the CFA of individual functions. Doubleclicking on an edge in the CFA will jump to the corresponding line in the source tab. For durther details, read the help text by clicking on the questionmark at the end of the tab bar.
  • ARG tab: shows the abstract reachability graph that was calculated by the analysis. Doubleclicking on a node will jump to the corresponding node in the CFA tab. For further details, read the help text by clicking on the questionmark at the end of the tab bar.
  • Witness tab (experimental): Some reports may also show a witness tab (if you generated it using a special, experimental branch of CPAchecker). This tab displays the generated witness graph. Doubleclicking on the edges/line numbers at the edges will jump to the corresponding line in the source tab. Doubleclicking on the nodes will jump to the corresponding CFA nodes (if the name matches, did I mention this feature is experimental?). Hovering above a state or edge will show all information that is saved in the witness about this element. For further details, read the help text by clicking on the questionmark at the end of the tab bar.
  • Source tab: contains a copy of the program's source code
  • Log tab: shows log messages generated by CPAchecker during the analysis
  • Statistics tab: Displays interesting statistics which may vary depending on the kind of analysis. For example this can be time taken by critical components like the solver or number of refinements.

Example 1: Correctness Report

The folder doc/examples contains a basic C source file.

int main() { int i = 0; int a = 0; while (1) { if (i == 20) { goto LOOPEND; } else { i++; a++; } if (i != a) { goto ERROR; } } LOOPEND: if (a != 20) { goto ERROR; } return (0); ERROR: return (-1); }

Execute CPAchecker with the default properties:

scripts/cpa{.sh|.bat} -config config/default.properties doc/examples/example.c

The example above should create a Report.html file inside the output directory.

This analysis formally proved the program to be correct, meaning that the location with the label ERROR: is unreachable. While this information is stated on the command line, CPAchecker also generates a detailed report that can be viewed in the browser. It tells us about the report in the last line of its output:

[...]
Verification result: TRUE. No property violation found by chosen configuration.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Report.html

You can find an online version the report for this particular execution of CPAchecker here.

Example 2: Counterexample Report

Consider the program example_withbug.c:

int main() { int i = 0; int a = 0; while (1) { if (i == 20) { goto LOOPEND; } else { i++; a++; } if (i != a) { goto ERROR; } } LOOPEND: if (a == 20) { goto ERROR; } return (0); ERROR: return (-1); }

The only change compared to example.c is that we negated the if-condition in line 20. The program is now guaranteed to reach the label ERROR: and thus also the generated report will contain different information. We execute CPAchecker for our new program with:

scripts/cpa{.sh|.bat} -config config/default.properties example_withbug.c

The example above should create a Counterexample.1.html file inside the output directory.

This time, we see a different conclusion at the end of the output:

Verification result: FALSE. Property violation (error label in line 21) found by chosen configuration.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Counterexample.1.html".

A copy of the generated report can be found here

results matching ""

    No results matching ""