Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
39 lines (35 sloc) 1.7 KB
OCaml (reasonably recent version; I use version 4.04.0)
OCamlbuild (reasonably recent version; I use version 0.10.1)
Camlp4 (matching your OCaml version)
OCamlgraph (reasonably recent version; I use version 1.8.7)
One or more of the following SMT-solvers:
yices, yices2, z3, cvc4, mathsat5
* z3 ML bindings:
To get z3 to work with kittel/koat directly, install the new ML
bindings. At this time (z3 stable version 4.3), they are only
available from the z3 source code repository on codeplex, in the
"ml-ng" branch.
To install them, check out this branch, configure z3 with
--ml (you will need ocamlfind, ocamlidl and some other libraries
as well, refer to the z3 documentation) and build as usual.
"make install" should then install the files into
/usr(/local)/lib/ocaml/$VERSION/, where VERSION corresponds to
your OCaml version.
You may need to add this path to the include path of your compiler,
cf. Makefile.
Use of APRON and the z3 ML bindings can be disabled by creating a
file "user.cfg". To disable use of APRON, add a line
"HAVE_APRON=false" to that file. To disable use of the z3 ML
bindings, add a line "HAVE_Z3=false" to that file.
Build instructions:
"make kittel" builds the termination analysis backend "kittel.native"
"make koat" builds the complexity analysis backend "koat.native"
"make convert" builds "convert.native" which converts Simple programs to C
You might need to modify the KITTEL_LIBPATH and KOAT_LIBPATH lines in the
Makefile to ensure that OCamlgraph and/or APRON is found (the
"-I,+ocamlgraph" resp. "-I,+apron" parts).