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.