regtests.sh 848 Bytes
Newer Older
1 2 3
#!/bin/sh
# regression tests for why3

4
TMP=$PWD/why3regtests.out
5
TMPERR=$PWD/why3regtests.err
6

7
cd `dirname $0`
8

MARCHE Claude's avatar
MARCHE Claude committed
9
res=0
10 11

run_dir () {
12 13 14
    for f in `ls $1/*/why3session.xml`; do
        d=`dirname $f`
	echo -n "Replaying "$d"... "
15 16 17 18 19 20 21 22 23 24 25
        ../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
MARCHE Claude's avatar
MARCHE Claude committed
26
	    res=1
27 28 29 30 31 32 33
	else
	    echo "OK"
	fi
    done
}

echo "=== Logic ==="
34
run_dir .
35 36
echo ""

37 38 39
# echo "=== BTS ==="
# run_dir bts
# echo ""
40

41 42 43
# echo "=== Programs ==="
# run_dir programs
# echo ""
44

MARCHE Claude's avatar
MARCHE Claude committed
45 46 47
# echo "=== Check Builtin traduction ==="
# run_dir check-builtin
# echo ""
48

MARCHE Claude's avatar
MARCHE Claude committed
49 50
exit $res

51