about summary refs log tree commit diff homepage
path: root/test/Concrete
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2014-09-12 15:46:23 -0700
committerDaniel Dunbar <daniel@zuster.org>2014-09-12 17:39:18 -0700
commitecb0ab1407f23e6d2403a8603613fdbf4101e519 (patch)
tree89c3632398a9448beabaae4e2235e6bfc54c5617 /test/Concrete
parentd2bb920c81e58c12d96a78495640bc793139fd3d (diff)
downloadklee-ecb0ab1407f23e6d2403a8603613fdbf4101e519.tar.gz
Add a README for the Concrete tests.
Diffstat (limited to 'test/Concrete')
-rw-r--r--test/Concrete/README.txt5
1 files changed, 5 insertions, 0 deletions
diff --git a/test/Concrete/README.txt b/test/Concrete/README.txt
new file mode 100644
index 00000000..3e4862e4
--- /dev/null
+++ b/test/Concrete/README.txt
@@ -0,0 +1,5 @@
+This directory contains tests which exist just to test the execution of Concrete
+code paths -- essentially, that we correctly implement the semantics of the LLVM
+IR language. The tests are run using a helper script ``ConcreteTest.py`` which
+builds the test bitcode, executes it using both ``lli`` and ``klee``, and checks
+that they got the same output.
\ No newline at end of file