1 files changed, 36 insertions, 0 deletions
diff --git a/test/TestRunner.sh b/test/TestRunner.sh
new file mode 100755
index 00000000..3e2cace4
--- /dev/null
+++ b/test/TestRunner.sh
@@ -0,0 +1,36 @@
+#!/bin/sh
+#
+#  TestRunner.sh - This script is used to run the deja-gnu tests exactly like
+#  deja-gnu does, by executing the Tcl script specified in the test case's 
+#  RUN: lines. This is made possible by a simple make target supported by the
+#  test/Makefile. All this script does is invoke that make target. 
+#
+#  Usage:
+#     TestRunner.sh {script_names}
+#
+#     This script is typically used by cd'ing to a test directory and then
+#     running TestRunner.sh with a list of test file names you want to run.
+#
+TESTPATH=`pwd`
+SUBDIR=""
+if test `dirname $1` = "." ; then
+  while test `basename $TESTPATH` != "test" -a ! -z "$TESTPATH" ; do
+    tmp=`basename $TESTPATH`
+    SUBDIR="$tmp/$SUBDIR"
+    TESTPATH=`dirname $TESTPATH`
+  done
+fi
+
+for TESTFILE in "$@" ; do 
+  if test `dirname $TESTFILE` = . ; then
+    if test -d "$TESTPATH" ; then
+      cd $TESTPATH
+      make check-one TESTONE="$SUBDIR$TESTFILE"
+      cd $PWD
+    else
+      echo "Can't find klee/test directory in " `pwd`
+    fi
+  else
+    make check-one TESTONE=$TESTFILE
+  fi
+done