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

4 5 6
REPLAYOPT=""

while test $# != 0; do
7
case "$1" in
8 9
  "--force")
        REPLAYOPT="$REPLAYOPT --force"
10
        ;;
11 12
  "--obsolete-only")
        REPLAYOPT="$REPLAYOPT --obsolete-only"
13
        ;;
14 15 16
  "--prover")
        REPLAYOPT="$REPLAYOPT --prover $2"
        shift
17 18 19 20 21
        ;;
  *)
        echo "$0: Unknown option '$1'"
        exit 2
esac
22 23
shift
done
24

25
TMP=$PWD/why3regtests.out
26
TMPERR=$PWD/why3regtests.err
27

28
cd `dirname $0`
29

30
# too early to do that
31
# REPLAYOPT="$REPLAYOPT --smoke-detector top"
32

MARCHE Claude's avatar
MARCHE Claude committed
33
res=0
34 35
export success=0
export total=0
36 37

run_dir () {
38 39
    for f in `ls $1/*/why3session.xml`; do
        d=`dirname $f`
40
	echo -n "Replaying $d ... "
41
        ../bin/why3replayer.opt -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP
42 43
        ret=$?
	if test "$ret" != "0"  ; then
44
	    echo -n "FAILED (ret code=$ret):"
45 46 47 48 49 50 51
            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
52
	    res=1
53
	else
54
	    echo -n "OK"
55
	    cat $TMP $TMPERR
56
            success=`expr $success + 1`
57
	fi
58
        total=`expr $total + 1`
59 60 61
    done
}

62 63
echo "=== Standard Library ==="
run_dir ../lib/why3
64 65
echo ""

66 67 68 69 70 71
# there's no session there...
# echo "=== Tests ==="
# run_dir tests
# run_dir tests-provers
# echo ""

72 73 74 75
echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""

76 77 78
echo "=== BTS ==="
run_dir bts
echo ""
79

Andrei Paskevich's avatar
Andrei Paskevich committed
80 81 82
echo "=== Logic ==="
run_dir logic
run_dir bitvectors "-I bitvectors"
83
echo ""
84

Andrei Paskevich's avatar
Andrei Paskevich committed
85 86 87 88 89
echo "=== Programs ==="
run_dir .
run_dir foveoos11-cm
run_dir hoare_logic
run_dir vacid_0_binary_heaps "-I vacid_0_binary_heaps"
90
echo ""
91

92
echo "Summary: $success/$total"
MARCHE Claude's avatar
MARCHE Claude committed
93 94
exit $res

95

96