In the Outgen folder you will find:
-
backend: it's the library and it should work as it is.
-
frontend: the scripts using the backend and it is likely that you might need to modify some of the stuff.
-
CBMC
-
gcov
-
Z3 in python3 (packages z3 and z3-tools).
-
Install pickle in python3
-
Install deap in python3.
-
Install pycparser, zss, deepcopy (copy), numpy, pandas,
-
Maybe packages: six.moves, cffi, configparser, collections, parser, pdb, hashlib
There are 2 examples in the Frontend:
-
OutGen.bash: OutGen algorithm
-
XORSample.bash: XORSample algorithm
Examples of running:
export DFT_HOME=/path/to/DFT/folder export EURI_HOME=/path/to/DFT/folder
export DFT_HOME=/home/menendez/data/infotestsoft/OutGen export EURI_HOME=/home/menendez/data/infotestsoft/OutGen
bash program.bash input_c_file function_name directory_for_results number_of_inputs
bash OutGen.bash 9-A-17766602.c main examples/ 10
This will create a directory for the program 9-A-17766602.c and inside you will find these types of files:
-
The preprocessed program *.pre.c.pre.c
-
The instrumented version of the program that you pass to cbmc *.cbmc.c
-
The ori is a version the equivalent version to the cbmc one but without the instrumentation: *.ori.c
-
The inputs *.c.inputs (you can read them using pickle, see below)
-
The constraints generated by CBMC (*z3) and their clean version for DFT (*clean.z3).
-
The finalTest*.c is the executable of the test.
-
The count.* gives you information about how many times you have reached the program point.
-
The coverage* gives you information about coverage extracted with gcov. The related files of coverage are: gcov, gcda, gcno