19 lines
911 B
Text
19 lines
911 B
Text
KLEE is a symbolic virtual machine built on top of the LLVM compiler
|
|
infrastructure.
|
|
|
|
Currently, there are two primary components:
|
|
* 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/.
|
|
* 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.
|
|
|
|
WWW: https://klee.github.io/
|