Data-Flow Analysis

In this section we take a quick look at how to call some of the data-flow analysis that CPAchecker can perform. We apply them to a simple example program (ex1.c) and take a brief look at the results.

int main() { int i = 0; int k = 0; int m = 7; while (i<4) { i++; k--; } m = m * 2; goto CHECK; i--; CHECK: return 0; }

For Windows Users: always add the following three settings when you call CPAchecker:

-setprop solver.solver=SMTInterpol -setprop cpa.predicate.encodeBitvectorAs=INTEGER -setprop cpa.predicate.encodeFloatAs=RATIONAL

This is neccessary because CPAchecker can use different solvers, and the default solver (MathSat5) is not yet available for the windows version. The three settings above configure CPAchecker to use another solver instead (SMTInterpol). Note that the results of the analysis may therefore differ, in some cases greatly.

Value Analysis

The basic value analysis tracks concrete values of the program variables where possible.

While there are more powerful variants of this analysis, we will only show a very basic one here.

Execute analysis:

scripts/cpa.sh -valueAnalysis-NoCegar-join examples/ex1.c -setprop analysis.checkCounterexamples=false

With Windows additional options are needed:

scripts/cpa.bat -valueAnalysis-NoCegar-join examples/ex1.c -setprop analysis.checkCounterexamples=false -setprop solver.solver=SMTInterpol -setprop cpa.predicate.encodeBitvectorAs=INTEGER -setprop cpa.predicate.encodeFloatAs=RATIONAL

The special options for windows will be omitted from now on, so add them yourself if you are using Windows.

CPAchecker generates a report for the analysis, a copy can be found here.

This analysis can e.g. be useful to identify unreachable code or locations where variables always have the same value. Note the following facts in the report:

  • ARG does not contain unreachable part (i--) (it is also not shown in the CFA)
  • for each reachable location, m has a certain, constant value
  • this is not true for i,k

Reaching-Definitions Analysis

Start the analysis like this:

scripts/cpa.sh -reachingdefinitionARG examples/ex1.c

The report contains information about the reaching definitions for each variable in the ARG.

Interval Analysis

Start the analysis like this:

scripts/cpa.sh -intervalAnalysis-join examples/ex1.c

In the report we can make the following observations:

  • in the Report.html, ARG nodes contain the possible intervals for each variable
  • e.g. note the loop head, which has main::i=[0;4]

Sign Analysis

Start the analysis like this:

scripts/cpa.sh -signAnalysis examples/ex1.c

In the generated report, the ARG nodes contain the sign information for each variable (that is either MINUS, ZERO, or PLUS)

results matching ""

    No results matching ""