CPA/Tiger – Tutorial

[Back to CPA/Tiger project website]

Disclaimer

The CPA/Tiger version used in this tutorial does not correspond to the ESOP’13 version.
The used version is adapted to recent changes in the CPAchecker architecture.

Installation

First, export the current version of CPA/Tiger from the CPAchecker SVN repository:
svn export http://cpachecker.googlecode.com/svn/branches/cpatiger/

Then, change into the cpatiger directory and run ant:
cd cpatiger
ant
Thereby missing dependencies get downloaded and afterwards the Java files get compiled.

Example

Using the following command line, CPA/Tiger will generate a test suite for basic block coverage for the program test/programs/benchmarks/ntdrivers-simplified/kbfiltr_simpl1_true-unreach-label_true-termination.cil.c:

./scripts/cpatiger.sh test/programs/benchmarks/ntdrivers-simplified/kbfiltr_simpl1_true-unreach-label_true-termination.cil.c

It will generate the following result:
Generated Test Cases:
p[__VERIFIER_nondet_int,9,0,10,4][__VERIFIER_nondet_long][__VERIFIER_nondet_uint][__VERIFIER_nondet_bool][__VERIFIER_nondet_char]
p[__VERIFIER_nondet_int,9,1,10,3,17,15,0,23,16,0,19,0][__VERIFIER_nondet_long][__VERIFIER_nondet_uint][__VERIFIER_nondet_bool]__VERIFIER_nondet_char]
p[__VERIFIER_nondet_int,9,1,4,4][__VERIFIER_nondet_long][__VERIFIER_nondet_uint][__VERIFIER_nondet_bool][__VERIFIER_nondet_char]
p[__VERIFIER_nondet_int,9,1,10,3,18,16,0,0,13,17,20,22,1,1][__VERIFIER_nondet_long][__VERIFIER_nondet_uint][__VERIFIER_nondet_bool][__VERIFIER_nondet_char]
p[__VERIFIER_nondet_int,9,-1,10,3,17,15,0,24,16,0,19,0][__VERIFIER_nondet_long][__VERIFIER_nondet_uint][__VERIFIER_nondet_bool][__VERIFIER_nondet_char]
p[__VERIFIER_nondet_int,9,-1,10,3,17,15,0,2,16,0,19,-1,-1][__VERIFIER_nondet_long][__VERIFIER_nondet_uint][__VERIFIER_nondet_bool][__VERIFIER_nondet_char]
p[__VERIFIER_nondet_int,9,0,10,3,18,16,0,0,13,17,20,22,-1,-1,0][__VERIFIER_nondet_long][__VERIFIER_nondet_uint][__VERIFIER_nondet_bool][__VERIFIER_nondet_char]
p[__VERIFIER_nondet_int,9,0,10,3,18,16,0,0,13,17,20,22,3,2,1][__VERIFIER_nondet_long][__VERIFIER_nondet_uint][__VERIFIER_nondet_bool][__VERIFIER_nondet_char]
p[__VERIFIER_nondet_int,9,1,10,3,18,16,0,0,13,17,20,22,0][__VERIFIER_nondet_long][__VERIFIER_nondet_uint][__VERIFIER_nondet_bool][__VERIFIER_nondet_char]
INTERN:
#Goals: 96
#Feasible: 69
#Infeasible: 27
#Imprecise: 0
#BugRevealing: 0
where a line
p[__VERIFIER_nondet_int,9,0,10,4][__VERIFIER_nondet_long][__VERIFIER_nondet_uint][__VERIFIER_nondet_bool][__VERIFIER_nondet_char]
describes a test case, where first the value 9, then 0, then 10, and finally the value 4 is read as input from the C function __VERIFIER_nondet_int. From such a test case, one can derive a corresponding implementation for __VERIFIER_nondet_int:

#include <stdlib.h>

int __VERIFIER_nondet_int() {
  static int i = -1;
  i++;
  switch (i) {
    case 0:
      return 9;
    case 1:
      return 0;
    case 2:
      return 10;
    case 3:
      return 4;
    default:
      exit(EXIT_FAILURE);
  }
}

Alternatively, one can also give a corresponding FQL query to obtain the same result as above:
./scripts/cpatiger.sh -fql 'COVER "EDGES(ID)*".EDGES(@BASICBLOCKENTRY)."EDGES(ID)*"' test/programs/benchmarks/ntdrivers-simplified/kbfiltr_simpl1_true-unreach-label_true-termination.cil.c


Contact

Address:
Andreas Holzer
Technische Universität Wien
Institut für Logic and Computation 192/4
Favoritenstraße 9–11
1040 Wien
Austria