regtests.sh 979 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
    for f in `ls $1/*/why3session.xml`; do
        d=`dirname $f`
14 15
	echo -n "Replaying $d ... "
        ../bin/why3replayer.opt $2 $d 2> $TMPERR > $TMP
16 17
        ret=$?
	if test "$ret" != "0"  ; then
18
	    echo -n "FAILED (ret code=$ret):"
19 20 21 22 23 24 25
            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
	else
28 29
	    echo -n "OK"
	    cat $TMP
30 31 32 33
	fi
    done
}

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

38 39 40
echo "=== BTS ==="
run_dir bts
echo ""
41

42 43 44
echo "=== Programs ==="
run_dir programs
echo ""
45

46 47
echo "=== Programs in their own subdir ==="
run_dir programs/vacid_0_binary_heaps "-I programs/vacid_0_binary_heaps"
48
echo ""
49

50 51 52
echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""
53

MARCHE Claude's avatar
MARCHE Claude committed
54 55
exit $res

56