diff --git a/bench/bench b/bench/bench index 2a404662f17ab6394e230ef8fe081add30a15386..90df948590ef0b314a21f0c8bd62e7e5593cc385 100755 --- a/bench/bench +++ b/bench/bench @@ -74,7 +74,7 @@ drivers () { valid_goals () { pgm="bin/why3prove$suffix" for f in $1/*.mlw; do - printf " "$f"... " + printf " $f... " if $pgm -t 10 -P alt-ergo $f | grep -q -v Valid; then echo "valid test $f failed!" echo "$pgm -P alt-ergo $f" @@ -89,7 +89,7 @@ valid_goals () { invalid_goals () { pgm="bin/why3prove$suffix" for f in $1/*.mlw; do - printf " "$f"... " + printf " $f... " if $pgm -t 3 -P alt-ergo $f | grep -q Valid; then echo "invalid test $f failed!" echo "$pgm -P alt-ergo $f" @@ -101,6 +101,21 @@ invalid_goals () { done } +replay () { + pgm="bin/why3replay$suffix" + for f in $1/*/; do + printf " $f... " + if $pgm $f > /dev/null; then + echo "ok" + else + echo "replay test failed!" + echo $pgm $f + $pgm $f + exit 1 + fi + done +} + execute () { pgm="bin/why3execute$suffix" printf " $1 $2... " @@ -214,6 +229,10 @@ goods examples/double_wp "-L examples/double_wp" goods examples/in_progress echo "" +echo "=== Checking replay (no prover) ===" +replay bench/replay +echo "" + echo "=== Checking valid goals ===" valid_goals bench/valid echo "" diff --git a/examples/bts/11244.why b/bench/replay/11244.why similarity index 100% rename from examples/bts/11244.why rename to bench/replay/11244.why diff --git a/examples/bts/11244/why3session.xml b/bench/replay/11244/why3session.xml similarity index 100% rename from examples/bts/11244/why3session.xml rename to bench/replay/11244/why3session.xml diff --git a/examples/bts/11244/why3shapes.gz b/bench/replay/11244/why3shapes.gz similarity index 100% rename from examples/bts/11244/why3shapes.gz rename to bench/replay/11244/why3shapes.gz diff --git a/examples/bts/13_compute_in.mlw b/bench/replay/13_compute_in.mlw similarity index 100% rename from examples/bts/13_compute_in.mlw rename to bench/replay/13_compute_in.mlw diff --git a/examples/bts/13_compute_in/why3session.xml b/bench/replay/13_compute_in/why3session.xml similarity index 85% rename from examples/bts/13_compute_in/why3session.xml rename to bench/replay/13_compute_in/why3session.xml index 78bd09b9c1cd24bd1e88d2be57f736c085863e1c..7f1ac31424481e70160a65459ec212ea762db5fb 100644 --- a/examples/bts/13_compute_in/why3session.xml +++ b/bench/replay/13_compute_in/why3session.xml @@ -3,7 +3,7 @@ "http://why3.lri.fr/why3session.dtd"> - + diff --git a/bench/replay/13_compute_in/why3shapes.gz b/bench/replay/13_compute_in/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..c808d4d2333494f7c08f37b9a0ee1c427e1e3019 Binary files /dev/null and b/bench/replay/13_compute_in/why3shapes.gz differ diff --git a/examples/bts/14_simpl.mlw b/bench/replay/14_simpl.mlw similarity index 100% rename from examples/bts/14_simpl.mlw rename to bench/replay/14_simpl.mlw diff --git a/examples/bts/14_simpl/why3session.xml b/bench/replay/14_simpl/why3session.xml similarity index 91% rename from examples/bts/14_simpl/why3session.xml rename to bench/replay/14_simpl/why3session.xml index 7cf71b9184af48937ac0e7ab43c82bcb489e6d31..7e9a9111bc57aa3d8881c24ce218ee658d38e10a 100644 --- a/examples/bts/14_simpl/why3session.xml +++ b/bench/replay/14_simpl/why3session.xml @@ -3,7 +3,7 @@ "http://why3.lri.fr/why3session.dtd"> - + diff --git a/bench/replay/14_simpl/why3shapes.gz b/bench/replay/14_simpl/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..490c773a8c96a5a0640acd6de065a6b8d5063d9a Binary files /dev/null and b/bench/replay/14_simpl/why3shapes.gz differ diff --git a/examples/bts/15_destruct_alg.mlw b/bench/replay/15_destruct_alg.mlw similarity index 100% rename from examples/bts/15_destruct_alg.mlw rename to bench/replay/15_destruct_alg.mlw diff --git a/examples/bts/15_destruct_alg/why3session.xml b/bench/replay/15_destruct_alg/why3session.xml similarity index 100% rename from examples/bts/15_destruct_alg/why3session.xml rename to bench/replay/15_destruct_alg/why3session.xml diff --git a/examples/bts/15_destruct_alg/why3shapes.gz b/bench/replay/15_destruct_alg/why3shapes.gz similarity index 100% rename from examples/bts/15_destruct_alg/why3shapes.gz rename to bench/replay/15_destruct_alg/why3shapes.gz diff --git a/examples/bts/17181.mlw b/bench/replay/17181.mlw similarity index 100% rename from examples/bts/17181.mlw rename to bench/replay/17181.mlw diff --git a/examples/bts/17181/why3session.xml b/bench/replay/17181/why3session.xml similarity index 100% rename from examples/bts/17181/why3session.xml rename to bench/replay/17181/why3session.xml diff --git a/examples/bts/17181/why3shapes.gz b/bench/replay/17181/why3shapes.gz similarity index 100% rename from examples/bts/17181/why3shapes.gz rename to bench/replay/17181/why3shapes.gz diff --git a/examples/bts/33_reload_trans.mlw b/bench/replay/33_reload_trans.mlw similarity index 81% rename from examples/bts/33_reload_trans.mlw rename to bench/replay/33_reload_trans.mlw index c44493462098caf1bb07768eb47e24eef8d7f19d..ea83f548fed07ff13033a495f3386ee4151d08cb 100644 --- a/examples/bts/33_reload_trans.mlw +++ b/bench/replay/33_reload_trans.mlw @@ -1,6 +1,5 @@ - module T goal G: False - -end \ No newline at end of file + +end diff --git a/examples/bts/33_reload_trans/why3session.xml b/bench/replay/33_reload_trans/why3session.xml similarity index 100% rename from examples/bts/33_reload_trans/why3session.xml rename to bench/replay/33_reload_trans/why3session.xml diff --git a/examples/bts/33_reload_trans/why3shapes.gz b/bench/replay/33_reload_trans/why3shapes.gz similarity index 100% rename from examples/bts/33_reload_trans/why3shapes.gz rename to bench/replay/33_reload_trans/why3shapes.gz diff --git a/examples/bts/13_compute_in/why3shapes.gz b/examples/bts/13_compute_in/why3shapes.gz deleted file mode 100644 index 80676f598207bb5857e87270b1adf55db62fb603..0000000000000000000000000000000000000000 Binary files a/examples/bts/13_compute_in/why3shapes.gz and /dev/null differ diff --git a/examples/bts/14_simpl/why3shapes.gz b/examples/bts/14_simpl/why3shapes.gz deleted file mode 100644 index d5285e4165fcc24e8a1a93fea5125298d7b16a47..0000000000000000000000000000000000000000 Binary files a/examples/bts/14_simpl/why3shapes.gz and /dev/null differ