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

Room: HD 03 13 (how to get there)
Phone: +43 (1) 58801 – 184 67
Email: ta.etysrofnull@rezloh
Web: http://forsyte.at/~holzer/

Latest News

FORSYTE’s 2018 paper awards

FORSYTE has had a quite successful year: Adrian Rebola Pardo and his co-authors received the IJCAR best paper award for their paper Extended Resolution Simulates DRAT, Mitra Tabaei Befrouei and her co-authors received an OOPSLA 2018 Distinguished Paper award for their paper Randomized Testing of Distributed Systems with Probabilistic Guarantees, and Thomas Pani received the […]

Continue reading

OOPSLA Distinguished Paper Award

Mitra Tabaei Befrouei and her co-authors from MPI-SWS Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Filip Niksic, received an OOPSLA’18 Distinguished Paper Award for their contribution “Randomized Testing of Distributed Systems with Probabilistic Guarantees” (Open Access article). Congratulations!

Continue reading

Zvonimir Rakamiric visiting FORSYTE

Prof. Zvonimir Rakamiric from the School of Computing at the University of Utah is spending his sabbatical with the FORSYTE group at TU Wien. He is generously sponsored by the Wolfgang Pauli Institute and a Pauli Fellow.

Continue reading

Full news archive