# HORNIX

Hornix is a verification tool that is based upon an LLVM extension also 
employing a CHC solver as a backend.

## Archive structure

The tool is available as a github repository: https://github.com/d3sformal/hornix 

It uses the `clang` and a customized `opt` binaries. Tho latter binary is
extended by a special pass `CHCTransform` enabling for transformation of the
LLVM bitcode into a system of constrained Horn clauses.

All the binaries (`clang`, `opt`, `z3`) are stored in the `bin` folder. The root
folder contains the launching script `hornix`, license files, and this
README file.

## Usage
./hornix <inputfile> - runs the verification on c or cpp code
./hornix --version   - prints the tool version and exits


