Commit 65cba90e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Do not skip directories in case of typo.

parent b34f9182
......@@ -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
......
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