KLEE with floating point support
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.travis fix metaSMT version Feb 21, 2017
autoconf Teach KLEE to link against UClibc's libm (i.e. math library). I guess no May 4, 2017
cmake
docs
examples Fixing missing include from get_sign.c Jan 10, 2014
include Teach `DiscretePDF` to take a comparison function that is used to do Aug 1, 2017
lib Teach `DiscretePDF` to take a comparison function that is used to do Aug 1, 2017
runtime [CMake] Fix #631 Mar 8, 2018
scripts Add script for printing bitvectors as floats. May 4, 2017
test Switch to correct Z3 solver API. `Z3_mk_simple_solver()` by-passes Jul 31, 2017
tools Teach KLEE to not warn about the floating point instrinsics May 4, 2017
unittests
utils More clean up. May 4, 2017
.clang-format Removed Language: Cpp entry from .clang-format due to incompatibility… Dec 24, 2015
.dockerignore Completely clean up how we patch Aachen's docker image. Instead May 4, 2017
.gitattributes
.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 Teach KLEE to link against UClibc's libm (i.e. math library). I guess no May 4, 2017
Dockerfile
LICENSE.TXT Slight updates in license file, acknowledging more recent contributions. Mar 3, 2015
Makefile Deliberately handicap the old build system so it cannot be used May 4, 2017
Makefile.common Teach KLEE to link against UClibc's libm (i.e. math library). I guess no May 4, 2017
Makefile.config.in Teach KLEE to link against UClibc's libm (i.e. math library). I guess no May 4, 2017
Makefile.rules
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 Teach KLEE to link against UClibc's libm (i.e. math library). I guess no May 4, 2017

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.