Commit 6ee734c1 authored by MARCHE Claude's avatar MARCHE Claude

new bench script using 'why3replayer -bench' and 'why3session html'

parent 6062e30c
......@@ -3,10 +3,9 @@
TMP=$PWD/why3bench.out
TMPERR=$PWD/why3bench.err
HTML=$PWD/why3bench.html
cd `dirname $0`
HTML=$PWD/why3bench.html
res=0
export success=0
......@@ -14,14 +13,15 @@ export total=0
echo '<html>' > $HTML
echo '<head><title>Why3 Bench</title></head>' >> $HTML
echo '<body>' > $HTML
echo '<h1>Why3 bench</h1>' > $HTML
echo '<body>' >> $HTML
echo '<h1>Why3 bench</h1>' >> $HTML
run_dir () {
echo '<h2>Directory '$1'</h2>' > $HTML
echo '<ul>' > $HTML
echo '<h2>Directory '$1'</h2>' >> $HTML
echo '<ul>' >> $HTML
for f in `ls $1/*/why3session.xml`; do
d=`dirname $f`
b=`basename $d`
echo -n "Benchmarking $d ... "
../bin/why3replayer.opt -bench $REPLAYOPT $2 $d 2> $TMPERR > $TMP
ret=$?
......@@ -35,40 +35,40 @@ run_dir () {
cat $TMP
fi
res=1
echo '<li>'$d' failed'
echo '<li>'$d' failed' >> $HTML
else
echo -n "OK"
../bin/why3session -bench $d 2> $TMPERR > $TMP
echo '<li><a href="'$d'">'$d'</a>'
cat $TMP
echo "OK"
success=`expr $success + 1`
../bin/why3session html $d 2> $TMPERR > $TMP
echo '<li><a href="'$d/$b'.html">'$d'</a>' >> $HTML
fi
total=`expr $total + 1`
done
echo '</ul>' > $HTML
echo '</ul>' >> $HTML
}
echo "=== Logic ==="
run_dir .
echo ""
# echo "=== BTS ==="
# run_dir bts
# echo ""
echo "=== BTS ==="
run_dir bts
echo ""
# echo "=== Programs ==="
# run_dir programs
# 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 "=== 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 "=== Check Builtin translation ==="
run_dir check-builtin
echo ""
echo '</body></html>' >> $HTML
echo "Summary: $success/$total"
exit $res
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment