CPAchecker's HTML Report

When CPAchecker terminates, it also generates a report in form a a HTML document. In this section, we take a closer look at the report and its features. 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:

[...]
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

Correctness Report

Generation

(This part is a recap of creating the checking our installation of CPAchecker/creating a correctness report

When testing whether our installation of CPAchecker is working, we applied an analysis on the program example.c that is shipped with CPAchecker:

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

We did this with the following command line call:

    scripts/cpa.sh -predicateAnalysis doc/examples/example.c

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.

Features

  • 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.

Counterexample Report

Generation

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 -predicateAnalysis examples/example_withbug.c

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

Features

The counterexample report contains all the features of the correctness report (look here). In addition, it shows a bar on the left with the trace of the counterexample. There you can inspect the values of the variables in each step by clicking on the "V" at the beginning of the line. You can also single-step through the trace while the currently displayed tab (ARG/CFA) will highlight the current state. This is very useful for understanding the cause of the error that was found.

results matching ""

    No results matching ""