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: holzer@forsyte.at
Web: http://forsyte.at/~holzer/

Latest News

Jens Pagel wins Bill McCune PhD Award

We congratulate Jens Pagel for receiving the 2021 Bill McCune PhD Award in Automated Reasoning! Jens graduated in 2020; his thesis on Decision procedures for separation logic: beyond symbolic heaps (supervised by Florian Zuleger) presents his substantial contributions to the theory of formal verification and automated reasoning, and to verifying heap-manipulating programs in particular.

Continue reading

Full news archive