Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 15 insertions, 15 deletions

diff --git a/README.txt b/README.txt
index 0c1a79e9..96d60a9e 100644
--- a/README.txt
+++ b/README.txt
@@ -1,24 +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.
+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/.
+  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.
+  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 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.
+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.
 
-For further information, see the docs in www/.
+For further information, see the webpage or docs in www/.