seahorn / Crab Llvm
Programming Languages
Projects that are alternatives of or similar to Crab Llvm
Clam: Crab for Llvm Abstraction Manager
Description
Clam is a static analyzer that computes inductive invariants for LLVM-based languages based on the Crab library. This branch supports LLVM 10.
The available documentation can be found in our wiki.
Docker
You can get the latest binary from Docker Hub (nightly built) using the command:
docker pull seahorn/clam-llvm10:nightly
Requirements for compiling from sources
Clam is written in C++ and uses heavily the Boost library. The main requirements are:
- Modern C++ compiler supporting c++14
- Boost >= 1.65
- GMP
- MPFR (if
-DCRAB_USE_APRON=ON
or-DCRAB_USE_ELINA=ON
)
In linux, you can install requirements typing the commands:
sudo apt-get install libboost-all-dev libboost-program-options-dev
sudo apt-get install libgmp-dev
sudo apt-get install libmpfr-dev
To run tests you need to install lit
and OutputCheck
. In Linux:
apt-get install python-pip
pip install lit
pip install OutputCheck
Compiling from sources and installation
The basic compilation steps are:
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=_DIR_ ../
cmake --build . --target crab && cmake ..
cmake --build . --target llvm && cmake ..
cmake --build . --target install
Clam provides several components that are installed via the extra
target. These components can be used by other projects outside of
Clam.
-
sea-dsa:
git clone https://github.com/seahorn/sea-dsa.git
sea-dsa
is the heap analysis used to translate LLVM memory instructions. Details can be found here and here. -
llvm-seahorn:
git clone https://github.com/seahorn/llvm-seahorn.git
llvm-seahorn
provides specialized versions ofInstCombine
andIndVarSimplify
LLVM passes as well as a LLVM pass to convert undefined values into nondeterministic calls.
The component sea-dsa
is mandatory and llvm-seahorn
is optional but highly
recommended. To include these external components, type instead:
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=_DIR_ ../
cmake --build . --target extra
cmake --build . --target crab && cmake ..
cmake --build . --target llvm && cmake ..
cmake --build . --target install
The Boxes/Apron/Elina domains require third-party libraries. To avoid the burden to users who are not interested in those domains, the installation of the libraries is optional.
-
If you want to use the Boxes domain then add
-DCRAB_USE_LDD=ON
option. -
If you want to use the Apron library domains then add
-DCRAB_USE_APRON=ON
option. -
If you want to use the Elina library domains then add
-DCRAB_USE_ELINA=ON
option.
Important: Apron and Elina are currently not compatible so you
cannot enable -DCRAB_USE_APRON=ON
and -DCRAB_USE_ELINA=ON
at the same time.
For instance, to install Clam with Boxes and Apron:
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=_DIR_ -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
cmake --build . --target extra
cmake --build . --target crab && cmake ..
cmake --build . --target ldd && cmake ..
cmake --build . --target apron && cmake ..
cmake --build . --target llvm && cmake ..
cmake --build . --target install
Checking installation
To run some regression tests:
cmake --build . --target test-simple