about summary refs log tree commit diff homepage
path: root/README-psychic.md
diff options
context:
space:
mode:
Diffstat (limited to 'README-psychic.md')
-rw-r--r--README-psychic.md15
1 files changed, 15 insertions, 0 deletions
diff --git a/README-psychic.md b/README-psychic.md
new file mode 100644
index 00000000..59985141
--- /dev/null
+++ b/README-psychic.md
@@ -0,0 +1,15 @@
+# KLEE-Psychic
+
+## Usage
+
+The metaprogram under test is to be built with Clang 12 and the following flags:
+
+    -g -O0 -Xclang -disable-O0-optnone
+    -fsanitize=undefined -fno-sanitize=local-bounds,function,vptr'
+
+Both native executable and LLVM bitcode are needed.
+For the bitcode, pass `-emit-llvm -c -DKLEE_RUNTIME` to Clang
+
+KLEE should then be run with the following flags:
+
+    --use-visitor-hash=0 --posix-runtime --libc uclibc --ubsan-runtime