(Work in progress) An abstract interpreter for an integer interval domain supporting basic operations
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
cbmc @ 240ae60
examples
include
scripts
src
.gitignore
.gitmodules
.travis.yml
CMakeLists.txt
LICENSE
README.md

README.md

Interval Domain Abstract Interpreter

Build Status

IntervalAI : An restricted Abstract Interpreter based on the integer interval domain

Prerequisites

  • CBMC 5.8 (included as a submodule)
  • g++ with C++11 support

Installing

Get the code. The directory containing this file shall be referred to as $INTERVALAI_ROOT

git clone --recurse-submodules git@github.com:GoodDeeds/IntervalAI.git

Build CBMC

cd $INTERVALAI_ROOT/IntervalAI/cbmc/src
make

Build IntervalAI

cd $INTERVALAI_ROOT/IntervalAI
mkdir build
cd build
cmake ..
make

Running the program

cd $INTERVALAI_ROOT/IntervalAI/build
./IntervalAI -m <mode> <goto-binary>