regtests.sh 1.92 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
export sessions=""
37
export shapes=""
38 39

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

66 67
echo "=== Standard Library ==="
run_dir ../lib/why3
68 69
echo ""

MARCHE Claude's avatar
MARCHE Claude committed
70
echo "=== Tests ==="
71 72
# there's no session there...
# run_dir tests
MARCHE Claude's avatar
MARCHE Claude committed
73 74
run_dir tests-provers
echo ""
75

76 77 78 79
echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""

80 81 82
echo "=== BTS ==="
run_dir bts
echo ""
83

Andrei Paskevich's avatar
Andrei Paskevich committed
84 85
echo "=== Logic ==="
run_dir logic
86
run_dir bitvectors "-L bitvectors"
87
echo ""
88

Andrei Paskevich's avatar
Andrei Paskevich committed
89 90 91 92
echo "=== Programs ==="
run_dir .
run_dir foveoos11-cm
run_dir hoare_logic
93
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
94
run_dir avl "-L avl"
95
echo ""
96

97 98
echo "Summary       : $success/$total"
echo "Sessions size : "`wc -cl $sessions | tail -1`
99
echo "Shapes   size : "`wc -cl $shapes | tail -1`
100

MARCHE Claude's avatar
MARCHE Claude committed
101 102
exit $res

103

104