diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-21 18:49:53 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-21 18:49:53 -0400 |
commit | 156e88c64620a1f48abdf0782035f4f25d28bfaa (patch) | |
tree | a1dc62bd14dea30f14f078660c48830a46289673 /test | |
parent | 6cd9e1a1219891fea61c5b97f2fe3105ac2ecdd7 (diff) |
run_regression using valgrind by setting VALGRIND=1
Diffstat (limited to 'test')
-rwxr-xr-x | test/regress/run_regression | 12 |
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" |