KLEE Symbolic Execution Engine
Clone or download
Permalink
Failed to load latest commit information.
cmake cmake: find_llvm, fix libraries with llvm-config 3.9 Sep 14, 2018
docs [CMake] Add `clean_doxygen` rule to clean up doxygen build tree and Oct 4, 2017
examples Removed unused file Sep 20, 2018
include Small changes to comments Oct 16, 2018
lib Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file i… Oct 16, 2018
runtime add support for klee-replay on OSX Oct 8, 2018
scripts Workaround for flaky coverage Oct 7, 2018
test tests: disable CompressedExprLogging on zlib-less systems Oct 17, 2018
tools Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file i… Oct 16, 2018
unittests Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file i… Oct 16, 2018
utils Support sanitizer suppression files with lit-based testing Jul 4, 2018
.clang-format Update clang-format standard for KLEE codebase to C++11 May 12, 2018
.codecov.yml Fix coverage generation Jan 30, 2018
.dockerignore Extensive updates to the build script for dependencies and docker Jul 4, 2018
.gitattributes Added .gitattribute file that takes care of line endings. Apr 9, 2015
.gitignore gitignore build May 26, 2017
.travis.yml travis: enable LLVM 4 testing Sep 18, 2018
CMakeLists.txt cmake/lit: add asan/non-asan, ubsan/non-ubsan flags Oct 10, 2018
LICENSE.TXT Slight updates in license file, acknowledging more recent contributions. Mar 3, 2015
NEWS Release notes for 1.4.0 Jul 21, 2017
README-CMake.md [CMake] Add option to set GTest include dir Mar 26, 2018
README.md [Travis-CI] Added codecov.io support Jan 16, 2018
TODO.txt Renamed .pc to .kquery (kleaver query) Nov 23, 2016

README.md

KLEE Symbolic Virtual Machine

Build Status Coverage

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.

For further information, see the webpage.