diff --git a/bench/bench b/bench/bench index 503fdc7d5b35301eb1eeed40930c08a49530ede1..5eb08a0d067de519ad7ffa0455393c91ad62836d 100755 --- a/bench/bench +++ b/bench/bench @@ -15,6 +15,7 @@ suffix=$1 goods () { pgm="bin/why3prove$suffix" ERROR= + test -d $1 || exit 1 rm -f bench_errors for f in $1/*.[wm][hl][yw] ; do printf " $f... " @@ -45,6 +46,7 @@ goods () { bads () { pgm="bin/why3prove$suffix" + test -d $1 || exit 1 for f in $1/*.[wm][hl][yw] ; do printf " $f... " if $pgm $2 $f > /dev/null 2>&1; then @@ -59,6 +61,7 @@ bads () { drivers () { pgm="bin/why3prove$suffix" + test -d $1 || exit 1 for f in $1/*.drv; do if [[ $f == drivers/ocaml*.drv ]]; then continue; fi if [[ $f == drivers/c.drv ]]; then continue; fi @@ -76,6 +79,7 @@ drivers () { valid_goals () { pgm="bin/why3prove$suffix" + test -d $1 || exit 1 for f in $1/*.mlw; do printf " $f... " if ! $pgm -t 15 -P alt-ergo $f > /dev/null 2>&1; then @@ -90,6 +94,7 @@ valid_goals () { invalid_goals () { pgm="bin/why3prove$suffix" + test -d $1 || exit 1 for f in $1/*.mlw; do printf " $f... " if $pgm -t 3 -P alt-ergo $f | grep -q Valid; then @@ -105,6 +110,7 @@ invalid_goals () { replay () { pgm="bin/why3replay$suffix" + test -d $1 || exit 1 for f in $1/*/; do printf " $f... " if $pgm $2 $f > /dev/null 2> /dev/null; then diff --git a/bench/typing/x-good/.keepme b/bench/typing/x-good/.keepme new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391