blob: 0c1a79e955d80c8454f4c4bb6ad2e0b4402e920e (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
//===----------------------------------------------------------------------===//
// Klee Symbolic Virtual Machine
//===----------------------------------------------------------------------===//
Daniel Dunbar
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. An emulation layer for the Linux system call interface, with
additional support for making parts of the operating environment
symbolic. This is found in models/simple.
Additionally, there is a simple library in runtime/ which supports
replaying computed inputs on native code. There is a more complicated
library in replay/ which supports running inputs computed as part of
the system call emulation layer natively -- setting up files, pipes,
etc. on the native system to match the inputs that the emulation layer
provided.
For further information, see the docs in www/.
|
