Angie project

Angie is a static analysis and verification framework, specifically for methods based on abstract interpretation.

• The current goal is to implement SMG abstraction extended paper, original paper
• Inspired by Predator
• Built primarily on top of LLVM but meant to be frontend-independent

The program is licensed under GNU LGPLv3+ and makes use of LLVM, Boost, Range-v3 [Range-v3-VS2015], GSL [GSL-lite] [V11-GSL], MemGraph [stripped fork] and possibly also Z3, CRoaring. All those are to my best knowledge distributed under compatible licenses.

Proud user of:

• https://github.com/petervanderdoes/gitflow-avh/

Dependencies install

First of all, memgraph submodule must be initialized and checked out:

git submodule init
git submodule update

For simple deployment, install_* helpers in utils directory will handle installation of CMake built or include-only libraries. Main motivation was repetitive fixing of Travis-CI and custom *nix server deployment. Currently needed dependencies to get Angie compiled:

# installation prefix for script, select any path, $HOME/local, ...
export PREFIX=$PWD/dependencies
# install missing libraries
sh utils/install_main.sh gtest
sh utils/install_main.sh boost
# install range-v3-vs2015 [MS VC14+ workaround support] or range-v3 [clang/gcc ISO C++14]
sh utils/install_main.sh range-v3-vs2015
# install gsl [C++14] or gsl-lite [C++11, custom fork with macros disabled]
sh utils/install_main.sh gsl-lite
# export or '-D'set CMAKE_PREFIX_PATH or CMAKE_INCLUDE_PATH
export CMAKE_PREFIX_PATH=$PREFIX

Build & Run

# set to your executables
COPT=opt
CLANGXX=clang++
CLANG=clang
export COPT CLANGXX CLANG
# configure and build the project
(bash ./compile-inputs-to-ll.sh <DIRECTORY_WITH_SOURCE_FILES>; mkdir tmp; cd tmp; cmake ../; make)
# ready to run!
# ./tmp/angie --help
./tmp/angie -f <FILE_TO_ANALYSE>

Contribution and credits

See CREDITS.txt

License

See LICENSE.txt