*ccti* (Curry Concolic Testing Interpreter) is a tool for automated generation of test cases for the functional logic language Curry.

To learn more about Curry take a look at the Curry report.

`18.12.2017:`

A first release of a Curry package including a prototype version of *ccti* is now available. You can install it using the Curry Package Manager.

*ccti* makes use of the *z3* SMT solver. Since *ccti* uses version 2.6 of the SMT-LIB standard which is not yet supported in the latest release version of *z3* (4.5.0), you have to install the latest version from the git repository. You can specify the installation directory for *z3* using the `--prefix`

option:

```
git clone https://github.com/Z3Prover/z3.git
cd z3
python scripts/mk_make.py --prefix=$HOME/z3/master
cd build
make
make install
```

After having installed *z3* please make sure that you add the *z3* binary to your path.

In order to install *ccti* you need the *PAKCS* Curry compiler (with type classes). You can either download the development release here or you can build *PAKCS* from source by checking out the latest version from gitlab using the following command:

`git clone https://git.ps.informatik.uni-kiel.de/curry/pakcs.git`

For installation of *PAKCS* please refer to the instructions provided in the pakcs folder (`INSTALL.txt`

for the tarball and `GITINSTALL.txt`

in case you build from source).

For Ubuntu/Debian systems there are also DEB packages of *PAKCS*. Here you can find out how to install them.

After *PAKCS* has been successfully installed, you can install *ccti* via the Curry Package Manager (*CPM*). In order to build *ccti* please make sure that the binary of the Curry Package Manager is in your path, e.g. by executing `cypm --help`

.

First, you should initialize/update your local package index using the command `cypm update`

. Afterwards you can install *ccti* by executing `cypm install ccti`

. The *ccti* binary will be installed to `$HOME/.cpm/bin`

.

Alternatively, you can check out the *ccti* package with `cypm checkout ccti`

, change into the corresponding directory, e.g. `cd $HOME/ccti`

and install *ccti* via the Makefile provided in the package by executing `make install`

. Afterwards you will find the binary of *ccti* in the `bin`

folder. In order to make it globally accessible you should add `$HOME/ccti/bin`

to your path.

To remove *ccti* simply execute `cypm uninstall ccti`

. In case you checked out the package and installed *ccti* locally you can simply remove the `ccti`

folder, e.g. assuming you installed it in your `$HOME`

directory:

`rm -rf $HOME/ccti`

In order to apply *ccti* for the automated generation of test cases for a Curry function you need to call its binary with Curry module. This Curry module has to include a `main`

function. The body of the `main`

function has to be a call (with concrete input data) to the function which shall be concolically tested. This call is required to initialize the concolic testing interpreter.

For instance, take a look at the following Curry module:

```
data Nat = IHi
| O Nat
| I Nat
deriving Eq
add :: Nat -> Nat -> Nat
add IHi y = succ y
add (O x) IHi = I x
add (O x) (O y) = O (add x y)
add (O x) (I y) = I (add x y)
add (I x) IHi = O (succ x)
add (I x) (O y) = I (add x y)
add (I x) (I y) = O (add (succ x) y)
succ :: Nat -> Nat
succ IHi = O IHi
succ (O x) = I x
succ (I x) = O (succ x)
main :: Nat
main = add IHi (I (O IHi))
```

This module includes a representation of positive binary numbers in Curry as well as an operation `add`

to add two binaries. In order to generate test cases for `add`

we provide a `main`

function with the initial call `add IHi (I (O IHi))`

.

Applying *ccti* on this module produces the following output including six test cases for `add`

:

```
examples> ccti Nat.curry
========================================================================================================================
Generating FlatCurry code
[1 of 2] Skipping Prelude ( /local/jrt/pakcs/lib/Prelude.curry, /local/jrt/pakcs/lib/.curry/Prelude.fcy )
[2 of 2] Compiling Nat ( Nat.curry, .curry/Nat.fcy )
========================================================================================================================
Reading FlatCurry file(s)
========================================================================================================================
Annotating case expressions with fresh identifiers
========================================================================================================================
Generating SMT-LIB declarations for FlatCurry types
========================================================================================================================
Beginning with concolic search
(Nat.add (Nat.O Nat.IHi) Nat.IHi = {Nat.I Nat.IHi})
(Nat.add (Nat.I Nat.IHi) (Nat.O Nat.IHi) = {Nat.I (Nat.O Nat.IHi)})
(Nat.add (Nat.I Nat.IHi) Nat.IHi = {Nat.O (Nat.O Nat.IHi)})
(Nat.add (Nat.I Nat.IHi) (Nat.I (Nat.O Nat.IHi)) = {Nat.O
(Nat.O (Nat.O Nat.IHi))})
(Nat.add (Nat.O Nat.IHi) (Nat.I (Nat.O Nat.IHi)) = {Nat.I (Nat.I Nat.IHi)})
(Nat.add Nat.IHi (Nat.I (Nat.O Nat.IHi)) = {Nat.O (Nat.I Nat.IHi)})
```

You can find the `Nat`

example as well as some other simple examples in the `examples`

folder of the *ccti* package which you can checkout via *CPM* by `cypm checkout ccti`

.

There are several options for *ccti*. You get an overview by executing `ccti --help`

.

For instance, you can change the coverage criterion used during concolic execution. Per default branch coverage is used. But there are examples in which this criterion is not sufficient, e.g. `Perm.curry`

. You can switch to function coverage by running the following command:

`ccti --cover=function Perm.curry`

If you want to take a look at the SMT-LIB scripts generated by *ccti* and sent to the *z3* SMT solver, you can produce a dump of these scripts by running `examples> ccti --dump-smt Nat.curry`

. The dump will be saved in a file in the hidden directory `examples/.smt/`

.