Commit 5cabcb2a authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Add option --prover to why3replayer and to regression suite for replaying part of the provers only.

parent b29c8db2
#!/bin/sh
# regression tests for why3
REPLAYOPT=""
while test $# != 0; do
case "$1" in
"-force")
REPLAYOPT="-force"
REPLAYOPT="$REPLAYOPT -force"
;;
"-obsolete-only")
REPLAYOPT="-obsolete-only"
REPLAYOPT="$REPLAYOPT -obsolete-only"
;;
"")
REPLAYOPT=""
"--prover")
REPLAYOPT="$REPLAYOPT --prover $2"
shift
;;
*)
echo "$0: Unknown option '$1'"
exit 2
esac
shift
done
TMP=$PWD/why3regtests.out
TMPERR=$PWD/why3regtests.err
......
......@@ -721,12 +721,16 @@ let rec goal_iter_proof_attempt_with_release ~release f g =
Mmetas_args.iter (fun _ t -> iter t.metas_goal) g.goal_metas;
if release then release_task g
let check_all ?(release=false) eS eT ~callback =
let check_all ?(release=false) ?filter eS eT ~callback =
dprintf debug "[Sched] check all@.%a@." print_session eS.session;
let todo = Todo.create [] push_report callback in
Todo.start todo;
let check_top_goal g =
let check a = check_external_proof eS eT todo a in
let check a =
let c = match filter with
| None -> true
| Some f -> f a in
if c then check_external_proof eS eT todo a in
goal_iter_proof_attempt_with_release ~release check g
in
PHstr.iter (fun _ file ->
......
......@@ -267,6 +267,7 @@ module Make(O: OBSERVER) : sig
val check_all:
?release:bool -> (** Can all the goal be release at the end? def: false *)
?filter:(O.key proof_attempt -> bool) ->
O.key env_session -> t ->
callback:((Ident.ident * Whyconf.prover * int * report) list -> unit) ->
unit
......
......@@ -42,7 +42,7 @@ let opt_stats = ref true
let opt_force = ref false
let opt_obsolete_only = ref false
let opt_bench = ref false
let opt_provers = ref []
......@@ -93,6 +93,10 @@ let spec = Arg.align [
" try to detect if the context is self-contradicting") ;
("--bench",
Arg.Set opt_bench, " run as bench (experimental)");
("--prover",
Arg.String (fun s ->
opt_provers := Whyconf.parse_filter_prover s :: !opt_provers),
"<prover> restrict replay to given prover");
("-s",
Arg.Clear opt_stats,
" do not print statistics") ;
......@@ -363,7 +367,14 @@ let add_to_check_no_smoke config found_obs env_session sched =
exit 1
end
in
M.check_all ~release:true ~callback env_session sched
if !opt_provers = [] then
M.check_all ~release:true ~callback env_session sched
else
let filter a =
List.exists
(fun p -> Whyconf.filter_prover p a.Session.proof_prover)
!opt_provers in
M.check_all ~release:true ~filter ~callback env_session sched
let add_to_check_smoke env_session sched =
let callback report =
......
Supports Markdown
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