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

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

19
TMP=$PWD/why3regtests.out
20
TMPERR=$PWD/why3regtests.err
21

22
cd `dirname $0`
23

24 25
# too early to do that
# REPLAYOPT="$REPLAYOPT -smoke-detector top"
26

MARCHE Claude's avatar
MARCHE Claude committed
27
res=0
28 29
export success=0
export total=0
30 31

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

56 57
echo "=== Tests ==="
run_dir tests
58 59 60 61 62 63 64
run_dir tests-provers
echo ""

echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""

65 66 67
echo "=== BTS ==="
run_dir bts
echo ""
68

Andrei Paskevich's avatar
Andrei Paskevich committed
69 70 71
echo "=== Logic ==="
run_dir logic
run_dir bitvectors "-I bitvectors"
72
echo ""
73

Andrei Paskevich's avatar
Andrei Paskevich committed
74 75 76 77 78
echo "=== Programs ==="
run_dir .
run_dir foveoos11-cm
run_dir hoare_logic
run_dir vacid_0_binary_heaps "-I vacid_0_binary_heaps"
79
echo ""
80

81
echo "Summary: $success/$total"
MARCHE Claude's avatar
MARCHE Claude committed
82 83
exit $res

84

85