Generic Model Checking for C Programs
GenMC is a stateless model checker for C programs that works on the level of LLVM Intermediate Representation.
This repository mirrors an internal repository and is only updated periodically. For changes between different versions please refer to the CHANGELOG.
Author: Michalis Kokologiannakis.
To pull a container containing GenMC from Docker Hub please issue the following command:
docker pull genmc/genmc
Building from source
The LLVM versions currently supported are: 3.8.1, 4.0.1, 6.0.1, 7.0.1, 8.0.1, 9.0.1, 10.0.1, 11.0.0.
In order to use the tool on a Debian-based installation, you will need the following packages:
autoconf automake clang libclang-dev llvm llvm-dev libffi-dev zlib1g-dev libedit-dev
Max OS X
brew, the following packages are necessary:
autoconf automake llvm libffi
For a default build issue:
autoreconf --install ./configure make
This will leave the
genmc executable in the
You can either run it from there (as in the examples below), or issue
Alternatively, the following following command will build the
executable in parallel and will also run a subset of all the tests
that come with the system to see if the system was built correctly or
make -j ctest
Mac OS X
For a default build issue:
autoreconf --install ./configure AR=llvm-ar make
To see a list of available options run:
To run a particular testcase run:
./src/genmc [options] <file>
For more detailed usage examples please refer to the manual.
Undefined references to symbols that involve types
This probably indicates that you are using an old version of LLVM with a new version of libstdc++. Configuring with the following flags should fix the problem:
CXXFLAGS="-D_GLIBCXX_USE_CXX11_ABI=0" ./configure --with-llvm=LLVM_PATH
Linking problems under Arch Linux:
Arch Linux does not provide the
libclang*.afiles required for linking against
clanglibraries. In order to for linking to succeed, please change the last line in
src/Makefile.amto the following:
genmc_LDADD = libgenmc.a -lclang-cpp
GenMC (with the exception of some files, see Exceptions) is distributed under the GPL, version 3 or (at your option) later. Please see the COPYING file for details on GPLv3.
Part of the code in the files listed below are originating from the LLVM Compiler Framework, version 3.5. These parts are licensed under the University of Illinois/NCSA Open Source License as well as under GPLv3. Please see the LLVMLICENSE file for details on the University of Illinois/NCSA Open Source License.
src/Interpreter.h src/Interpreter.cpp src/Execution.cpp src/ExternalFunctions.cpp
Additionally, the files within the
include directory are licensed
under their own licenses.
Please see the respective header for more information on a specific file's license.
For feedback, questions, and bug reports please send an e-mail to
michalis AT mpi-sws DOT org.