Commit 6ec46d38 authored by MARCHE Claude's avatar MARCHE Claude

an hopefully more robust nightly bench script

parent e73db6d3
......@@ -4,7 +4,8 @@ OUT=$PWD/nightly-bench.out
REPORT=$PWD/nightly-bench.report
notify() {
mail -s "Why3 nightly bench" why3-commits@lists.gforge.inria.fr < $REPORT
# mail -s "Why3 nightly bench" why3-commits@lists.gforge.inria.fr < $REPORT
mail -s "test Why3 nightly bench" Claude.Marche@inria.fr < $REPORT
# cat $REPORT
exit 0
}
......
......@@ -2,6 +2,7 @@
# regression tests for why3
TMP=$PWD/why3regtests.out
TMPERR=$PWD/why3regtests.err
cd `dirname $0`
......@@ -11,9 +12,17 @@ run_dir () {
for f in `ls $1/*/why3session.xml`; do
d=`dirname $f`
echo -n "Replaying "$d"... "
if ! ../bin/why3replayer.opt $d 2>/dev/null > $TMP ; then
echo "FAILED:"
cat $TMP
../bin/why3replayer.opt $d 2> $TMPERR > $TMP
ret=$?
if test "$ret" != "0" ; then
echo "FAILED (ret code=$ret):"
out=`head -1 $TMP`
if test -z "$out" ; then
echo "standard error: (standard output empty)"
cat $TMPERR
else
cat $TMP
fi
res=1
else
echo "OK"
......@@ -25,13 +34,13 @@ echo "=== Logic ==="
run_dir .
echo ""
echo "=== BTS ==="
run_dir bts
echo ""
# echo "=== BTS ==="
# run_dir bts
# echo ""
echo "=== Programs ==="
run_dir programs
echo ""
# echo "=== Programs ==="
# run_dir programs
# echo ""
echo "=== Check Builtin traduction ==="
run_dir check-builtin
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment