Commit 88a2bd9b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add option --merging-only to why3 replay and use it on all the examples in the bench.

parent 546cf540
...@@ -107,12 +107,12 @@ replay () { ...@@ -107,12 +107,12 @@ replay () {
pgm="bin/why3replay$suffix" pgm="bin/why3replay$suffix"
for f in $1/*/; do for f in $1/*/; do
printf " $f... " printf " $f... "
if $pgm $f > /dev/null; then if $pgm $2 $f > /dev/null 2> /dev/null; then
echo "ok" echo "ok"
else else
echo "replay test failed!" echo "replay test failed!"
echo $pgm $f echo $pgm $2 $f
$pgm $f $pgm $2 $f
exit 1 exit 1
fi fi
done done
...@@ -236,6 +236,22 @@ echo "" ...@@ -236,6 +236,22 @@ echo ""
echo "=== Checking replay (no prover) ===" echo "=== Checking replay (no prover) ==="
replay bench/replay replay bench/replay
replay examples/bts --merging-only
replay examples/tests --merging-only
replay examples/tests-provers --merging-only
replay examples/check-builtin --merging-only
replay examples/logic --merging-only
replay examples --merging-only
replay examples/foveoos11-cm --merging-only
replay examples/WP_revisited --merging-only
replay examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps --merging-only"
replay examples/bitvectors "-L examples/bitvectors --merging-only"
replay examples/avl "-L examples/avl --merging-only"
#replay examples/to_port/verifythis_2016_matrix_multiplication "-L examples/to_port/verifythis_2016_matrix_multiplication --merging-only"
replay examples/double_wp "-L examples/double_wp --merging-only"
replay examples/ring_decision "-L examples/ring_decision --merging-only"
#replay examples/in_progress --merging-only
#replay examples/in_progress/multiprecision "-L examples/in_progress/multiprecision --merging-only"
echo "" echo ""
echo "=== Checking valid goals ===" echo "=== Checking valid goals ==="
......
...@@ -36,6 +36,7 @@ let opt_stats = ref true ...@@ -36,6 +36,7 @@ let opt_stats = ref true
let opt_force = ref false let opt_force = ref false
let opt_obsolete_only = ref false let opt_obsolete_only = ref false
let opt_use_steps = ref false let opt_use_steps = ref false
let opt_merging_only = ref false
(* (*
let opt_bench = ref false let opt_bench = ref false
*) *)
...@@ -78,7 +79,10 @@ let option_list = [ ...@@ -78,7 +79,10 @@ let option_list = [
" replay using recorded number of proof steps (when possible)"); " replay using recorded number of proof steps (when possible)");
("--obsolete-only", ("--obsolete-only",
Arg.Set opt_obsolete_only, Arg.Set opt_obsolete_only,
" replay only if session is obsolete") ; " replay only if session is obsolete");
("--merging-only",
Arg.Set opt_merging_only,
" check merging of session");
("-P", ("-P",
Arg.String (fun s -> Arg.String (fun s ->
opt_provers := Whyconf.parse_filter_prover s :: !opt_provers), opt_provers := Whyconf.parse_filter_prover s :: !opt_provers),
...@@ -376,6 +380,8 @@ let () = ...@@ -376,6 +380,8 @@ let () =
*) *)
if found_obs then eprintf "[Warning] session is obsolete@."; if found_obs then eprintf "[Warning] session is obsolete@.";
if found_detached then eprintf "[Warning] found detached goals or theories or transformations@."; if found_detached then eprintf "[Warning] found detached goals or theories or transformations@.";
if !opt_merging_only then
exit (if found_detached then 1 else 0);
add_to_check_no_smoke found_detached found_obs cont; add_to_check_no_smoke found_detached found_obs cont;
Debug.dprintf debug "[Replay] starting scheduler@."; Debug.dprintf debug "[Replay] starting scheduler@.";
Unix_scheduler.Unix_scheduler.main_loop ~prompt:"" (fun _ -> ()); Unix_scheduler.Unix_scheduler.main_loop ~prompt:"" (fun _ -> ());
......
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