Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

bench.sh 1.54 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
#!/bin/sh
# bench for why3

TMP=$PWD/why3bench.out
TMPERR=$PWD/why3bench.err
HTML=$PWD/why3bench.html

cd `dirname $0`


res=0
export success=0
export total=0

echo '<html>' > $HTML
echo '<head><title>Why3 Bench</title></head>' >> $HTML
echo '<body>' > $HTML
echo '<h1>Why3 bench</h1>' > $HTML
 
run_dir () {
    echo '<h2>Directory '$1'</h2>' > $HTML
    echo '<ul>' > $HTML
    for f in `ls $1/*/why3session.xml`; do
        d=`dirname $f`
	echo -n "Benchmarking $d ... "
        ../bin/why3replayer.opt -bench $REPLAYOPT $2 $d 2> $TMPERR > $TMP
        ret=$?
	if test "$ret" != "0"  ; then
	    echo -n "FAILED (ret code=$ret):"
            out=`head -1 $TMP`
            if test -z "$out" ; then
               echo "standard error: (standard output empty)"
               cat $TMPERR
            else
	       cat $TMP
            fi
	    res=1
            echo '<li>'$d' failed'
	else
	    echo -n "OK"
            ../bin/why3session -bench $d 2> $TMPERR > $TMP
            echo '<li><a href="'$d'">'$d'</a>'
	    cat $TMP
            success=`expr $success + 1`
	fi
        total=`expr $total + 1`
    done
    echo '</ul>' > $HTML
}

echo "=== Logic ==="
run_dir .
echo ""

# echo "=== BTS ==="
# run_dir bts
# echo ""

# echo "=== Programs ==="
# run_dir programs
# echo ""

# echo "=== Programs in their own subdir ==="
# run_dir programs/vacid_0_binary_heaps "-I programs/vacid_0_binary_heaps"
# run_dir hoare_logic "-I hoare_logic"
# echo ""

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

echo "Summary: $success/$total"
exit $res