summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2014-07-21 18:49:53 -0400
committerKshitij Bansal <kshitij@cs.nyu.edu>2014-07-21 18:49:53 -0400
commit156e88c64620a1f48abdf0782035f4f25d28bfaa (patch)
treea1dc62bd14dea30f14f078660c48830a46289673 /test
parent6cd9e1a1219891fea61c5b97f2fe3105ac2ecdd7 (diff)
run_regression using valgrind by setting VALGRIND=1
Diffstat (limited to 'test')
-rwxr-xr-xtest/regress/run_regression12
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression
index f0ffd765d..d234153a3 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -41,6 +41,10 @@ while [ $# -gt 2 ]; do
shift
done
+[[ "$VALGRIND" = "1" ]] && {
+ wrapper="libtool --mode=execute valgrind $wrapper"
+}
+
cvc4=$1
benchmark_orig=$2
benchmark="$benchmark_orig"
@@ -250,7 +254,15 @@ fi
# we have to actual error file same treatment as other files. differences in
# versions of echo/bash were causing failure on some platforms and not on others
+# (also grep out valgrind output, if 0 errors reported by valgrind)
actual_error=$(cat $errfile)
+if [[ "$VALGRIND" = "1" ]]; then
+ #valgrind_output=$(cat $errfile|grep -E "^==[0-9]+== "|)
+ valgrind_num_errors=$(cat $errfile|grep -E "^==[0-9]+== "|tail -n1|awk '{print $4}')
+ echo "valgrind errors (not suppressed): $valgrind_num_errors" 1>&2
+
+ ((valgrind_num_errors == 0)) && actual_error=$(echo "$actual_error"|grep -vE "^==[0-9]+== ")
+fi
if [ -z "$actual_error" ]; then
# in case expected stderr output is empty, make sure we don't differ
# by a newline, which we would if we echo "" >"$experrfile"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback