diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-04-04 23:03:52 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-04-04 23:03:52 +0000 |
| commit | ff53861016427723a7c29e9bbca6f497b4556164 (patch) | |
| tree | 4ed798e2f7dfa31283f7d14d44e70c77badf6b75 /test/regress/run_regression | |
| parent | 42c58baf0a2a96c1f3bd797d64834d02adfb9a59 (diff) | |
* Addressed issues brought up in Chris's review of Morgan's
NodeManager (bug #65). Better documentation, etc.
* As part of this, removed NodeManager::mkVar() (which created a
variable of unknown type). This requires changes to lots of unit
tests, which were using this function.
* Performed some review of parser code (my code review #73).
+ I changed the way exceptions were caught and rethrown in
src/parser/input.cpp.
+ ParserExceptions weren't being properly constructed (d_line and
d_column weren't intiialized and could contain junk, leading to
weird error messages). Fixed.
* Fix to the current working directory used by run_regression script.
Makes exceptional output easier to match against (in expected error
output).
* (configure.ac) Ensure that CFLAGS has -fexceptions in it, in case we
compile any C code and don't use the C++ compiler.
Diffstat (limited to 'test/regress/run_regression')
| -rwxr-xr-x | test/regress/run_regression | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index 65ab6c31a..439c8e6c9 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -77,7 +77,17 @@ else echo "$expected_error" >"$experrfile" fi -("$cvc4" --segv-nospin "$benchmark"; echo $? >"$exitstatusfile") > "$outfile" 2> "$errfile" +cvc4dir=`dirname "$cvc4"` +cvc4dirfull=`cd "$cvc4dir" && pwd` +if [ -z "$cvc4dirfull" ]; then + error "getting directory of \`$cvc4 !?" +fi +cvc4base=`basename "$cvc4"` +cvc4full="$cvc4dirfull/$cvc4base" +( cd `dirname "$benchmark"`; + "$cvc4full" --segv-nospin `basename "$benchmark"`; + echo $? >"$exitstatusfile" +) > "$outfile" 2> "$errfile" diffs=`diff -u "$expoutfile" "$outfile"` diffexit=$? |