klee: Add run.sh --help and run.sh -s

1 files changed, 42 insertions, 9 deletions

diff --git a/test/symbolic/klee/run.sh b/test/symbolic/klee/run.sh
index c143cd0624..0234a935b5 100755
--- a/test/symbolic/klee/run.sh
+++ b/test/symbolic/klee/run.sh
@@ -10,13 +10,43 @@ KLEE_TEST_DIR="$PROJECT_SOURCE_DIR/test/symbolic/klee"
 KLEE_BIN_DIR="$PROJECT_BINARY_DIR/klee"
 KLEE_OUT_DIR="$KLEE_BIN_DIR/out"
 
+help() {
+  echo "Usage:"
+  echo
+  echo "  $0 -c fname"
+  echo "  $0 fname"
+  echo "  $0 -s"
+  echo
+  echo "First form compiles executable out of test/symbolic/klee/{fname}.c."
+  echo "Compiled executable is placed into build/klee/{fname}. Must first"
+  echo "successfully compile Neovim in order to generate declarations."
+  echo
+  echo "Second form runs KLEE in a docker container using file "
+  echo "test/symbolic/klee/{fname.c}. Bitcode is placed into build/klee/a.bc,"
+  echo "results are placed into build/klee/out/. The latter is first deleted if"
+  echo "it exists."
+  echo
+  echo "Third form runs ktest-tool which prints errors found by KLEE via "
+  echo "the same container used to run KLEE."
+}
+
 main() {
   local compile=
-  if test "$1" = "-c" ; then
+  local print_errs=
+  if test "$1" = "--help" ; then
+    help
+    return
+  fi
+  if test "$1" = "-s" ; then
+    print_errs=1
+    shift
+  elif test "$1" = "-c" ; then
     compile=1
     shift
   fi
-  local test="$1" ; shift
+  if test -z "$print_errs" ; then
+    local test="$1" ; shift
+  fi
 
   local includes=
   includes="$includes -I$KLEE_TEST_DIR"
@@ -36,14 +66,17 @@ main() {
   test -d "$KLEE_BIN_DIR" || mkdir -p "$KLEE_BIN_DIR"
 
   if test -z "$compile" ; then
-    test -d "$KLEE_OUT_DIR" && rm -r "$KLEE_OUT_DIR"
     local line1='cd /image'
-    line1="$line1 && $(echo clang \
-      $includes $defines \
-      -o "$KLEE_BIN_DIR/a.bc" -emit-llvm -g -c \
-      "$KLEE_TEST_DIR/$test.c")"
-    line1="$line1 && klee --libc=uclibc --posix-runtime "
-    line1="$line1 '--output-dir=$KLEE_OUT_DIR' '$KLEE_BIN_DIR/a.bc'"
+    if test -z "$print_errs" ; then
+      test -d "$KLEE_OUT_DIR" && rm -r "$KLEE_OUT_DIR"
+
+      line1="$line1 && $(echo clang \
+        $includes $defines \
+        -o "$KLEE_BIN_DIR/a.bc" -emit-llvm -g -c \
+        "$KLEE_TEST_DIR/$test.c")"
+      line1="$line1 && klee --libc=uclibc --posix-runtime "
+      line1="$line1 '--output-dir=$KLEE_OUT_DIR' '$KLEE_BIN_DIR/a.bc'"
+    fi
     local line2="for t in '$KLEE_OUT_DIR'/*.err"
     line2="$line2 ; do ktest-tool --write-ints"
     line2="$line2 \"\$(printf '%s' \"\$t\" | sed -e 's@\\.[^/]*\$@.ktest@')\""