KLEE Symbolic Virtual Machine
C++ C Makefile CMake Python LLVM Other
Latest commit b2f93ff Feb 14, 2017 @andreamattavelli andreamattavelli committed with delcypher Increased the type size for the stop-after-n-instructions option to a…
…void too strict limitations (LLVM >= 3.0)
Permalink
Failed to load latest commit information.
.travis [TravisCI] Modify TravisCI/Docker build scripts to support doing ASan… Jan 19, 2017
autoconf Fix two issues with AC_LINK_IFELSE for metaSMT: Dec 28, 2016
cmake [cmake] add PATH_SUFFIXES needed to find z3 on Fedora Jan 28, 2017
docs Implement a CMake based build system for KLEE. Nov 7, 2016
examples Fixing missing include from get_sign.c Jan 10, 2014
include Refactoring code to improve readability by using UINT32/64_C macros Feb 14, 2017
lib Increased the type size for the stop-after-n-instructions option to a… Feb 14, 2017
runtime Merge pull request #506 from delcypher/travis_asan_ubsan Feb 13, 2017
scripts Added missing copyright headers per klee/issue #301 Feb 24, 2016
test Fix linker compatibility under macOS Feb 14, 2017
tools [CMake] Rename "integrationtests" to "systemtests". Jan 16, 2017
unittests Added unit tests for ReadExpr::create() to check that constant foldin… Feb 14, 2017
utils Renamed .pc to .kquery (kleaver query) Nov 23, 2016
.clang-format Removed Language: Cpp entry from .clang-format due to incompatibility… Dec 24, 2015
.dockerignore Add the Dockerfile to `.dockerignore` so that changes the Dockerfile Nov 7, 2016
.gitattributes Added .gitattribute file that takes care of line endings. Apr 9, 2015
.gitignore Ignore some generated files that will be visible if doing an in source Dec 13, 2015
.travis.yml [TravisCI] Modify TravisCI/Docker build scripts to support doing ASan… Jan 19, 2017
CMakeLists.txt [CMake] Remove `ENABLE_TESTS` CMake cache option. Jan 18, 2017
Dockerfile [TravisCI] Modify TravisCI/Docker build scripts to support doing ASan… Jan 19, 2017
LICENSE.TXT Slight updates in license file, acknowledging more recent contributions. Mar 3, 2015
Makefile During install, install the klee intrinsic header file which is Apr 25, 2015
Makefile.common Fix the Autoconf/Makefile build system when building with coverage Jan 19, 2017
Makefile.config.in Support gzip-based compression of raw_outstreams Jul 8, 2016
Makefile.rules Remove undocumented and unused `check-local`, `check-dg` and `check-lit` Jan 16, 2017
MetaSMT.mk rename the configure option --with-metasmt-default-solver to --with-m… Jun 10, 2016
NEWS Release notes for 1.3.0 Nov 30, 2016
README-CMake.md [CMake] Remove `ENABLE_TESTS` CMake cache option. Jan 18, 2017
README.md Added link to coverage information Aug 10, 2015
TODO.txt Renamed .pc to .kquery (kleaver query) Nov 23, 2016
configure Fix two issues with AC_LINK_IFELSE for metaSMT: Dec 28, 2016

README.md

KLEE Symbolic Virtual Machine

Build Status

KLEE is a symbolic virtual machine built on top of the LLVM compiler infrastructure. Currently, there are two primary components:

  1. The core symbolic virtual machine engine; this is responsible for executing LLVM bitcode modules with support for symbolic values. This is comprised of the code in lib/.

  2. A POSIX/Linux emulation layer oriented towards supporting uClibc, with additional support for making parts of the operating system environment symbolic.

Additionally, there is a simple library for replaying computed inputs on native code (for closed programs). There is also a more complicated infrastructure for replaying the inputs generated for the POSIX/Linux emulation layer, which handles running native programs in an environment that matches a computed test input, including setting up files, pipes, environment variables, and passing command line arguments.

Coverage information can be found here.

For further information, see the webpage.