* Node::isAtomic() now looks at an "atomic" attribute of arguments

  instead of assuming it's atomic based on kind.  Atomicity is
  determined at node building time.  Fixes bug #81.  If this is
  determined to make node building too slow, we can allocate another
  attribute "AtomicHasBeenComputed" to lazily compute atomicity.

* TheoryImpl<> has gone away.  Theory implementations now derive from
  Theory directly and share a single RegisteredAttr attribute for term
  registration (which shouldn't overlap: every term is "owned" by
  exactly one Theory).  Fixes bug #79.

* Additional atomicity tests in ExprBlack unit test.

* More appropriate whitebox testing for attribute ID assignment
  (AttributeWhite unit test).

* Better (and more correct) assertion checking in NodeBuilderBlack.

* run-regression script now checks exit status against what's provided
  in "% EXIT: " gesture in .cvc input files, and stderr against
  "% EXPECT-ERROR: ".  These can be used to support intended failures.
  Fixes bug #84.  Also add "% EXIT: " gestures to all .cvc regressions
  in repository.

* Solved some "control reaches end of non-void function" warnings in
  src/parser/bounded_token_buffer.cpp by replacing
  "AlwaysAssert(false)" with "Unreachable()" (which is known
  statically to never return normally).

* Regression tests now use the cvc4 binary under
  builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which
  may not be properly installed yet at that point of the build.
  (Partially fixes bug #46.)

* -fvisibility=hidden is now included by configure.ac instead of each
   Makefile.am, which will make it easier to support platforms
   (e.g. cygwin) that do things a different way.

* TheoryUF code formatting.  (re: my code review bug #64)

* CDMap<> is leaking memory again, pending a fix for bug #85 in the
  context subsystem.  (To avoid serious errors, can't free context
  objects.)

* add ContextWhite unit test for bug #85 (though it's currently
  "defanged," awaiting the bugfix)

* Minor documentation, other cleanup.

1 files changed, 49 insertions, 16 deletions

diff --git a/test/regress/run_regression b/test/regress/run_regression
index 2be776b3f..65ab6c31a 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -44,35 +44,68 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
   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'"
+  expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
+  if [ -z "$expected_output" -a -z "$expected_error" ]; then
+    error "cannot determine expected output of \`$benchmark': " \
+          "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures"
   fi
   expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'`
+  if [ -z "$expected_exit_status" ]; then
+    error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
+  fi
 else
   error "benchmark \`$benchmark' must be *.cvc or *.smt"
 fi
 
-expfile=`mktemp -t cvc4_expected.XXXXXXXXXX`
-outfile=`mktemp -t cvc4_output.XXXXXXXXXX`
-echo "$expected_output" >"$expfile"
+expoutfile=`mktemp -t cvc4_expect_stdout.XXXXXXXXXX`
+experrfile=`mktemp -t cvc4_expect_stderr.XXXXXXXXXX`
+outfile=`mktemp -t cvc4_stdout.XXXXXXXXXX`
+errfile=`mktemp -t cvc4_stderr.XXXXXXXXXX`
+exitstatusfile=`mktemp -t cvc4_exitstatus.XXXXXXXXXX`
+if [ -z "$expected_output" ]; then
+  # in case expected stdout output is empty, make sure we don't differ
+  # by a newline, which we would if we echo "" >"$expoutfile"
+  touch "$expoutfile"
+else
+  echo "$expected_output" >"$expoutfile"
+fi
+if [ -z "$expected_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"
+  touch "$experrfile"
+else
+  echo "$expected_error" >"$experrfile"
+fi
 
-# echo "$cvc4" --segv-nospin "$benchmark"
-"$cvc4" --segv-nospin "$benchmark" > "$outfile"
+("$cvc4" --segv-nospin "$benchmark"; echo $? >"$exitstatusfile") > "$outfile" 2> "$errfile"
 
-diffs=`diff -u "$expfile" "$outfile"`
+diffs=`diff -u "$expoutfile" "$outfile"`
 diffexit=$?
-rm -f "$expfile"
+diffserr=`diff -u "$experrfile" "$errfile"`
+diffexiterr=$?
+exit_status=`cat "$exitstatusfile"`
+
+rm -f "$expoutfile"
+rm -f "$experrfile"
 rm -f "$outfile"
+rm -f "$errfile"
+rm -f "$exitstatusfile"
+
+exitcode=0
 if [ $diffexit -ne 0 ]; then
-  echo "$prog: error: differences between expected and actual output"
+  echo "$prog: error: differences between expected and actual output on stdout"
   echo "$diffs"
-  exit 1
+  exitcode=1
+fi
+if [ $diffexiterr -ne 0 ]; then
+  echo "$prog: error: differences between expected and actual output on stderr"
+  echo "$diffserr"
+  exitcode=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
+if [ "$exit_status" != "$expected_exit_status" ]; then
+  echo  "$prog: error: expected exit status \`$expected_exit_status' but got \`$exit_status'"
+  exitcode=1
 fi
 
+exit $exitcode