This is part of the homework assignment described here.
The goal was to implement a test generation tool similar to CUTE/DART for a subset of C.
The tool was implemented in OCaml. We prefered to use the STP solver instead of the recommended yices however we would like to add support for more solvers, starting with alt-ergo.
Note that we used STP and it's OCaml bindings found here not the ones from STP's site.
** Dependencies **
To compile:
$ cd stp
$ ./clean-install.sh
$ cd ../
$ cd cil
$ ./configure
$ make
$ cd cute
$ make
$ cd mycute
$ make
To test:
$ cd cute
$ ./cutec tests/testme.c
$ tests/testme.exe
$ ./cute ../mycute/mycute tests/testme.exe -i 10