Skip to content

Latest commit

 

History

History
17 lines (12 loc) · 962 Bytes

README.md

File metadata and controls

17 lines (12 loc) · 962 Bytes

Utils for CHC encodings of C programs with pointers using CBMC

The tool implements a CHC-to-CHC transformation based on FreqHorn and Z3.

Installation

Compiles with gcc-7 (on Linux) and clang-1001 (on Mac). Assumes preinstalled GMP, and Boost (libboost-system1.74-dev) packages. Additionally, armadillo package to get candidates from behaviors.

  • cd aeval ; mkdir build ; cd build
  • cmake ../
  • make to build dependencies (Z3)
  • make (again) to build MCHC

The mchc binary can be found at build/tools/mchc/mchc. After the alias analysis, the chc.smt2 file is generated (make sure to move it to a secure place, otherwise it will be rewritten in the next run). Run mchc --help for the usage info.