Commit f466ece0 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Partly adapt the bench to the new commands.

parent a0ea5237
...@@ -1554,7 +1554,7 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \ ...@@ -1554,7 +1554,7 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
# desactivé car requiert findlib # desactivé car requiert findlib
# if test -d examples/runstrat ; then \ # if test -d examples/runstrat ; then \
# $(MAKE) test-runstrat.@OCAMLBEST@ ; fi # $(MAKE) test-runstrat.@OCAMLBEST@ ; fi
bash bench/bench "bin/why3.@OCAMLBEST@" bash bench/bench ".@OCAMLBEST@"
@if test "@enable_coq_tactic@" = "yes"; then \ @if test "@enable_coq_tactic@" = "yes"; then \
echo "=== checking the Coq tactic ==="; \ echo "=== checking the Coq tactic ==="; \
$(MAKE) test-coq-tactic.@OCAMLBEST@; fi $(MAKE) test-coq-tactic.@OCAMLBEST@; fi
......
...@@ -7,9 +7,10 @@ ...@@ -7,9 +7,10 @@
# export WHY3DATA=. # export WHY3DATA=.
# export WHY3LOADPATH=theories # export WHY3LOADPATH=theories
pgm=$1 suffix=$1
goods () { goods () {
pgm="bin/why3prove$suffix"
for f in $1/*.[wm][hl][yw] ; do for f in $1/*.[wm][hl][yw] ; do
echo -n " $f... " echo -n " $f... "
# running Why # running Why
...@@ -26,6 +27,7 @@ goods () { ...@@ -26,6 +27,7 @@ goods () {
} }
bads () { bads () {
pgm="bin/why3prove$suffix"
for f in $1/*.[wm][hl][yw] ; do for f in $1/*.[wm][hl][yw] ; do
echo -n " $f... " echo -n " $f... "
if $pgm $2 $f > /dev/null 2>&1; then if $pgm $2 $f > /dev/null 2>&1; then
...@@ -39,6 +41,7 @@ bads () { ...@@ -39,6 +41,7 @@ bads () {
} }
drivers () { drivers () {
pgm="bin/why3prove$suffix"
for f in $1/*.drv; do for f in $1/*.drv; do
if [[ $f == drivers/ocaml*.drv ]]; then continue; fi if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
echo -n " $f... " echo -n " $f... "
...@@ -53,6 +56,7 @@ drivers () { ...@@ -53,6 +56,7 @@ drivers () {
} }
valid_goals () { valid_goals () {
pgm="bin/why3prove$suffix"
for f in $1/*.mlw; do for f in $1/*.mlw; do
echo -n " "$f"... " echo -n " "$f"... "
if $pgm -t 10 -P alt-ergo $f | grep -q -v Valid; then if $pgm -t 10 -P alt-ergo $f | grep -q -v Valid; then
...@@ -67,6 +71,7 @@ valid_goals () { ...@@ -67,6 +71,7 @@ valid_goals () {
} }
invalid_goals () { invalid_goals () {
pgm="bin/why3prove$suffix"
for f in $1/*.mlw; do for f in $1/*.mlw; do
echo -n " "$f"... " echo -n " "$f"... "
if $pgm -t 3 -P alt-ergo $f | grep -q Valid; then if $pgm -t 3 -P alt-ergo $f | grep -q Valid; then
...@@ -81,6 +86,7 @@ invalid_goals () { ...@@ -81,6 +86,7 @@ invalid_goals () {
} }
execute () { execute () {
pgm="bin/why3execute$suffix"
echo -n "$1 $2... " echo -n "$1 $2... "
if $pgm $1 --exec $2 > /dev/null 2>&1; then if $pgm $1 --exec $2 > /dev/null 2>&1; then
echo "ok" echo "ok"
...@@ -123,6 +129,7 @@ extract_and_run () { ...@@ -123,6 +129,7 @@ extract_and_run () {
} }
list_stuff () { list_stuff () {
pgm="bin/why3$suffix"
echo -n "$1 " echo -n "$1 "
if $pgm $1 > /dev/null 2>&1; then if $pgm $1 > /dev/null 2>&1; then
echo "ok" echo "ok"
...@@ -164,8 +171,8 @@ goods examples/logic ...@@ -164,8 +171,8 @@ goods examples/logic
goods examples goods examples
goods examples/foveoos11-cm goods examples/foveoos11-cm
goods examples/hoare_logic goods examples/hoare_logic
goods examples/vacid_0_binary_heaps "-I examples/vacid_0_binary_heaps" goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-I examples/bitvectors" goods examples/bitvectors "-L examples/bitvectors"
goods examples/in_progress goods examples/in_progress
echo "" echo ""
......
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