diff options
author | Daniel Dunbar <daniel@zuster.org> | 2009-03-15 05:28:32 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2009-03-15 05:28:32 +0000 |
commit | f2822ba876defa890c06e179b6f015b9d483c719 (patch) | |
tree | 90316e70a68daf3baddbe92318205c0daa873da6 /README.txt | |
download | klee-f2822ba876defa890c06e179b6f015b9d483c719.tar.gz |
Stub out klee project.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@67019 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'README.txt')
-rw-r--r-- | README.txt | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/README.txt b/README.txt new file mode 100644 index 00000000..0c1a79e9 --- /dev/null +++ b/README.txt @@ -0,0 +1,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/. |