REQUIREMENTS
============
Intel's PIN tool (version 3.2-81205), which is available here: http://software.intel.com/sites/landingpage/pintool/downloads/pin-3.2-81205-gcc-linux.tar.gz

GDB (tested on version 7.10)

GCC g++ (tested on version 5.2.1)

Bash (tested on version 4.3.42)

Plain CBMC (you can download the binary from here: http://www.cprover.org/cbmc/). This is required if you want to compare our performace against CBMC (i.e. to run the script run_all.sh)

Input file that will be provided to the tool should be "compilable" (i.e. "gcc file.c -lpthread" should work)

RUNNING
=======
Once you have above requirements modify the file 'common' to update 'PIN_DIR' to point to root directory of PIN tool downloaded and 'PLAIN_CBMC_DIR' to point to the directory consisting of normal cbmc binary.

There are two bash scripts run.sh and run_all.sh

run.sh
------
This script can be used to run only our tool. You can either pass a single ANSI-C file (with '-f' option) or pass multiple files present in a file. You can pass the unwind count with '-u' option. Optionally, you can specify unwind count in the file (if you are using file list) by separating it by a space. Refer 'file_list_example' for an example.

A typical run looks like:
"./run.sh -f example.c -u 10"
This takes example.c from current directory and unwind depth of 10.

run_all.sh
----------
This script runs our tool and plain cbmc, which can be used for comparision. Its usage is as shown below:

Usage: run_all.sh file_list

The unwind count has to be present in file_list. Refer 'file_list_example' for an example.


DETAILS
=======
Given an ANSI-C file example.c we first compile it and then run the binary under pin tool 'trace.so' to get multiple executions. The execution log is then parsed(parse program) to get write set(defuse and defuse_cbmc files in log_* directory). This write set is passed to CBMC along with example.c and unwind depth provided.
While running under the pin tool we may observe assertion failure. In such case we still go ahead and get invariants. 

Description of files:
cbmc		     CBMC binary with our change
example.c	     an example program, which is safe and unwind count 10
file_list_example    another example to show how multiple files can be passed
macros.h	     macros used by pin tool
parse.cpp	     parser of executions generated by pin tool
trace.cpp	     pin tool
verifier.c	     our definitions of some of the common functions used in benchmarks
run_all.sh           run our changes and plain cbmc for comparision

Source of CBMC changes can be found here: https://github.com/sumanthsprabhu/cbmc/tree/rf_underapprox