diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-04 19:01:55 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-04 19:01:55 +0000 |
commit | 3203c9bf8ec818b287c8b4030bb4b71d48ede9f1 (patch) | |
tree | cf737891c4f8edaaa05c7a362849165c8a20b5d5 /test/regress/run_regression | |
parent | 70a4ae1e6a7dae928e2ec83bd190b9b81e11bf02 (diff) |
test infrastructure updated for multiple-level regressions
Diffstat (limited to 'test/regress/run_regression')
-rwxr-xr-x | test/regress/run_regression | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression new file mode 100755 index 000000000..4cf9f07cf --- /dev/null +++ b/test/regress/run_regression @@ -0,0 +1,77 @@ +#!/bin/bash +# +# Morgan Deters <mdeters@cs.nyu.edu> +# for the CVC4 project +# +# usage: +# +# run_regression cvc4-binary [ benchmark.cvc | benchmark.smt ] +# +# Runs benchmark and checks for correct exit status and output. +# + +prog=`basename "$0"` + +if [ $# != 2 ]; then + echo "usage: $prog cvc4-binary [ benchmark.cvc | benchmark.smt ]" >&2 + exit 1 +fi + +cvc4=$1 +benchmark=$2 + +function error { + echo "$prog: error: $*" + exit 1 +} + +if ! [ -x "$cvc4" ]; then + error "\`$cvc4' doesn't exist or isn't executable" >&2 +fi +if ! [ -r "$benchmark" ]; then + error "\`$benchmark' doesn't exist or isn't readable" >&2 +fi + +if expr "$benchmark" : '.*\.smt$' &>/dev/null; then + if grep '^ *:status *sat' &>/dev/null; then + expected_output=sat + expected_exit_status=10 + elif grep '^ *:status *unsat' &>/dev/null; then + expected_output=unsat + expected_exit_status=20 + else + error "cannot determine status of \`$benchmark'" + fi +elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then + expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` + if [ -z "$expected_output" ]; then + error "cannot determine status of \`$benchmark'" + fi + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'` +else + error "benchmark \`$benchmark' must be *.cvc or *.smt" +fi + +expfile=`mktemp -t cvc4test.exp.XXXXXXXXXX` +outfile=`mktemp -t cvc4test.out.XXXXXXXXXX` +echo "$expected_output" >"$expfile" + +echo "$cvc4" --segv-nospin "$benchmark" +"$cvc4" --segv-nospin "$benchmark" | tee "$outfile" +exit_status=$? + +diffs=`diff -u "$expfile" "$outfile"` +rm -f "$expfile" +rm -f "$outfile" +if [ $? -ne 0 ]; then + echo "$prog: error: differences between expected and actual output" + echo "$diffs" + exit 1 +fi + +if [ -n "$expected_exit_status" ]; then + if [ $exit_status != "$expected_exit_status" ]; then + error "expected exit status \`$expected_exit_status' but got \`$exit_status'" + fi +fi + |