lambda2023/cute-homework

Concolic testing for C programs

CUTE-homework

This is part of the homework assignment described here.

The goal was to implement a test case 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.

Note that we used STP and it's OCaml bindings found here not the ones from STP's site.

Dependencies

• Assignment files
• STP

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