diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-06-30 13:35:53 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-06-30 13:35:53 +0000 |
| commit | 9f6f847830ae7b5f24305b597025517cb576699b (patch) | |
| tree | 731910205d95f86dbb53fbbe836b4e041f8b1474 | |
| parent | 4375b60d5df794b2c6193f3892185ea181a0748d (diff) | |
Support for failing .smt and .smt2 regressions (and other examples with
additional output). If the benchmark file has '% EXPECT: ' gestures,
like for cvc regressions, that is used (after being stripped out so that
the cvc4 smt parser never sees these special lines). However, this can
be a pain, since then you can't run the regression manually on the
command line (since it fails to parse). So if there is another file
in the same directory as $benchmark called $benchmark.expect, that is
scanned for '% EXPECT: ' etc., and the benchmark file is used verbatim.
| -rwxr-xr-x | test/regress/run_regression | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index b4fc43be6..b26792a78 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -34,7 +34,14 @@ fi tmpbenchmark= if expr "$benchmark" : '.*\.smt$' &>/dev/null; then - if grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" "$benchmark"; then + if test -e "$benchmark.expect"; then + expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` + expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | sed 's,^% EXIT: ,,'` + if [ -z "$expected_exit_status" ]; then + error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" + fi + elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" "$benchmark"; then expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'` @@ -54,7 +61,15 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then - if grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" "$benchmark"; then + if test -e "$benchmark.expect"; then + expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` + expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | sed 's,^% EXIT: ,,'` + if [ -z "$expected_exit_status" ]; then + error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" + fi + benchmark=$tmpbenchmark + elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" "$benchmark"; then expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'` |