Hi. Welcome to VERMEER, a tool for Tracing and Explaining Faulty C programs. There are a few things you will need to do before you can use VERMEER. 1) First, you will need to install Z3 and ensure that it is available on your path -- download the package from https://z3.codeplex.com/ -- add it to your PATH -- you can test if it works by trying $ z3 --version which should give you something like: Z3 version 4.3.2 2) Secondly, you need to set the environment variable VERMEER_PATH to the same directory this file is in. On my linux box, this meant adding the line export VERMEER_PATH="/home/dsn/Research/fault-localization" to my .bashrc. you can test if it is set correctly by running $ echo $VERMEER_PATH /home/dsn/Research/fault-localization We highly recommend adding $VERMEER_PATH/bin to your PATH environment variable. For Bash, $ export PATH=$VERMEER_PATH/bin:$PATH 3) You will also need a recent version of: -- ocaml compiler -- PERL -- JAVA -- gcc -- ocaml findlib You can test for these by running $ ocamlc -version 3.12.1 $ java -version java version "1.7.0_65" $ perl -version This is perl 5, version 14, subversion 2 (v5.14.2) $ gcc --version gcc (Ubuntu/Linaro 4.6.3-1ubuntu5) 4.6.3 $ ocamlfind Consult your distribution's documentation on how to install those if they are missing. NOTE: the versions listed above are the versions that we tested VERMEER with. It is highly likely that any more recent version will also work. 4) You will need to have Ocamlgraph installed $ cd ocamlgraph-1.8.6 $ ./configure $ make $ sudo make install-findlib 5) Now you need to build the tool. $ cd $VERMEER_PATH/cil-1.7.3 $ ./configure $ make 6) Now you're ready to try an example. Vermeer consists of a number of different passes, including the cilly compiler, the gcc compiler, executing a a.out and processing the result using perl scripts. In order to make it easier to run, we have provided shell scripts that automatically call the relevant parts in the correct order. $ cd $VERMEER_PATH/examples/simple Here we assume that you have put $VERMEER_PATH/bin to your PATH, where all the scripts used below reside. Try running the "simple.c" example from the demo video. First, make a linear trace $ runlinear simple This should create a file in simple_dir called simple.postlinear.c $ runconcrete simple This should create a file in simple_dir called simple.postconcrete.c $ runexplain simple This should create a file in simple_dir called explanation.txt which contains the explanation. (FYI, the default explanation algorithm generates a trace different from the one in the demo video.) You can choose which algorithm to use for explanation generation among three available ones (see the paper for details), e.g., $ runexplain -a explain simple $ runexplain -a fast_abs simple $ runexplain -a full_abs simple 7) Now let's try an example from the SIR repository cd $VERMEER_PATH\examples\sed $ runlinear sed This should create a file sed.postlinear.c $ runconcrete sed This should create a file sed.postconcrete.c You will need to add an assertion ('dsn_assert') at the end of this file. dsn_assert(re_search_2__6__mem_1406 > 1024); This should go right before the comment: // Looks like the concretized trace ran into a crash. $ runexplain sed Check out explanation.txt for the reduced trace. ****************** Possible Problems ********************************** We have developed and tested VERMEER on 64bit Ubuntu Linux 12.04. We believe that it should work on any linux box. We have not tested it on Mac or Windows. There are known issues with using the Cilly C front-end on Mac, due to OS X's use of non-standard C constructs. DSN - I got a make error, which I fixed using http://stackoverflow.com/questions/23498237/compile-program-for-32bit-on-64bit-linux-os-causes-fatal-error libgtk2.0-dev liblablgtk2-ocaml-dev liblablgtk2-gnome-ocaml-dev ****************** Benchmark Licence ********************************** A note about the SIR repository benchmarks. These benchmarks are the property of the University of Nebraska, who have generously allowed us to use them. Please do not redistribute these files without their permission. See the file LICENSE for details.