From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 21 Jul 2014 22:49:53 +0000 (-0400)
Subject: run_regression using valgrind by setting VALGRIND=1
X-Git-Tag: cvc5-1.0.0~6691
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=156e88c64620a1f48abdf0782035f4f25d28bfaa;p=cvc5.git

run_regression using valgrind by setting VALGRIND=1
---

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"