An abstract interpreter for an integer interval domain supporting basic operations for simple C programs
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
cbmc @ 240ae60
examples
include
scripts
src
.gitignore
.gitmodules
.travis.yml
CMakeLists.txt
LICENSE
README.md

README.md

IntervalAI

Build Status

An abstract interpreter based on the integer interval domain for simple C programs

Setup

Prerequisites

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

Building the project

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

$ git clone --recurse-submodules https://github.com/GoodDeeds/IntervalAI $INTERVALAI_ROOT

Build CBMC

$ cd $INTERVALAI_ROOT/IntervalAI/cbmc/src
$ make

Build IntervalAI

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

Running IntervalAI

Go to INTERVALAI_ROOT/IntervalAI/build. Then, use

$ ./IntervalAI -m <mode> <goto-binary>

Information on modes available, and the restrictions on the input, can be found by using

$ ./IntervalAI -h

License

This code is provided under the MIT License.

Note: The code has a few known bugs, which are in the process of getting resolved.