Compile HiFrog for Theory Refinement

Installation:

1. Firstly install OpenSMT2 as a library to be used in HiFrog binary; configure & install OpenSMT2 as follows:

​​OpenSMT2 depends on the following libraries: zlibgmp,gmpxxreadlineflex (if you need more info regarding installation of these libraries you may follow these instructions)

To compile OpenSMT2, first download it via:

$ git clone https://scm.ti-edu.ch/repogit/opensmt2.git

Enter the opsntm2 folder and run the configure script:

$ cd opensmt2
$ autoreconf --force --install
$ ./configure

Then run make and install.

$ make
$ sudo make install

2. Get the git repository of hifrog:

​  $ git clone -b master https://scm.ti-edu.ch/repogit/hifrog

3. Compile the cprover framework in the hifrog repository:

   $ cd hifrog/trunk/cprover/src; make clean; make
4. Check the in hifrog/trunk/cprover/src/Makefile and compile hifrog
   $ cd funfrog; make clean; make -f Makefile-no-itp

A small hint: During the compilation, if you happen to see such message "make: *** No rule to make target `../cpp/cpp.a', needed by `hifrog'. Stop.", please go the mentioned directory cd ../cpp and do "make" there. Then again do make in funfrog directory.

Run HiFrog to use theory refinement algorithm.

./hifrog --theoref --bitwidth <n> --heuristic <n> --unwind <n> --claim <n> --custom <ids> <your code-to-verify>

./hifrog --theoref --bitwidth 32 --unwind 10 --heuristic 4 --claim 1 filename.c



You may read on the parameters: heuristic, unwind, claim and custom on ./hifrog --help

 

The git repository we use for HiFrog is hosted at https://scm.ti-edu.ch/projects/hifrog.

 

 

** If you need any assistance, please contact us **

sepideh.a65[at]gmail.com or
karine.even_mendoza[at]kcl.ac.uk