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

4 5 6 7 8 9 10 11 12 13 14 15
case "$1" in
  "-force")
        REPLAYOPT="-force"
        ;;
  "")
        REPLAYOPT=""
        ;;
  *)
        echo "$0: Unknown option '$1'"
        exit 2
esac

16
TMP=$PWD/why3regtests.out
17
TMPERR=$PWD/why3regtests.err
18

19
cd `dirname $0`
20

21

MARCHE Claude's avatar
MARCHE Claude committed
22
res=0
23 24
export success=0
export total=0
25 26

run_dir () {
27 28
    for f in `ls $1/*/why3session.xml`; do
        d=`dirname $f`
29
	echo -n "Replaying $d ... "
30
        ../bin/why3replayer.opt $REPLAYOPT $2 $d 2> $TMPERR > $TMP
31 32
        ret=$?
	if test "$ret" != "0"  ; then
33
	    echo -n "FAILED (ret code=$ret):"
34 35 36 37 38 39 40
            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
41
	    res=1
42
	else
43 44
	    echo -n "OK"
	    cat $TMP
45
            success=`expr $success + 1`
46
	fi
47
        total=`expr $total + 1`
48 49 50
    done
}

51 52 53
echo "=== Logic ==="
run_dir .
echo ""
54

55 56 57
echo "=== BTS ==="
run_dir bts
echo ""
58

59 60 61
echo "=== Programs ==="
run_dir programs
echo ""
62

63 64
echo "=== Programs in their own subdir ==="
run_dir programs/vacid_0_binary_heaps "-I programs/vacid_0_binary_heaps"
65
echo ""
66

67 68 69
echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""
70

71
echo "Summary: $success/$total"
MARCHE Claude's avatar
MARCHE Claude committed
72 73
exit $res

74

75