about summary refs log tree commit diff homepage
path: root/README.txt
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-03-15 05:28:32 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-03-15 05:28:32 +0000
commitf2822ba876defa890c06e179b6f015b9d483c719 (patch)
tree90316e70a68daf3baddbe92318205c0daa873da6 /README.txt
downloadklee-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.txt24
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/.