Commit a634b6b4 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'issue_270' into 'master'

why3prove: Make the output of counterexamples readable by default

Closes #270

See merge request !94
parents a8a049d7 202a88dd
......@@ -71,7 +71,7 @@ run () {
echo "Strongest Postcondition" > "$f.out"
printf "Strongest Postcondition ${file_path} ($1)... "
fi
$dir/../bin/why3prove.opt --debug print_model_attrs${wp_sp} -P "$1,counterexamples" --timelimit 1 -a split_vc "${file_path}.mlw" | \
$dir/../bin/why3prove.opt --json --debug print_model_attrs${wp_sp} -P "$1,counterexamples" --timelimit 1 -a split_vc "${file_path}.mlw" | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
......
......@@ -136,7 +136,7 @@ let result1 : Call_provers.prover_result =
(* prints Alt-Ergo answer *)
let () = printf "@[On task 1, Alt-Ergo answers %a@."
Call_provers.print_prover_result result1
(Call_provers.print_prover_result ~json_model:false) result1
(* END{callprover} *)
(* BEGIN{calltimelimit} *)
......@@ -192,7 +192,7 @@ let result3 =
alt_ergo_driver task3)
let () = printf "@[On task 3, alt-ergo answers %a@."
Call_provers.print_prover_result result3
(Call_provers.print_prover_result ~json_model:false) result3
(* quantifiers: let's build "forall x:int. x*x >= 0" *)
(* BEGIN{quantfmla1} *)
......@@ -230,7 +230,7 @@ let result4 =
alt_ergo_driver task4)
let () = printf "@[On task 4, alt-ergo answers %a@."
Call_provers.print_prover_result result4
(Call_provers.print_prover_result ~json_model:false) result4
(* build a theory with all these goals *)
......
......@@ -300,7 +300,7 @@ let () =
alt_ergo_driver t)
in
printf "@[On task %d, alt-ergo answers %a@."
i Call_provers.print_prover_result r;
i (Call_provers.print_prover_result ~json_model:false) r;
i+1
)
1 my_tasks
......
......@@ -162,14 +162,17 @@ let print_prover_status fmt = function
let print_steps fmt s =
if s >= 0 then fprintf fmt ", %d steps" s
let print_prover_result fmt {pr_answer = ans; pr_status = status;
pr_output = out; pr_time = t;
pr_steps = s; pr_model = m} =
let print_prover_result ~json_model fmt {pr_answer = ans; pr_status = status;
pr_output = out; pr_time = t;
pr_steps = s; pr_model = m} =
let print_attrs = Debug.test_flag debug_attrs in
fprintf fmt "%a (%.2fs%a)" print_prover_answer ans t print_steps s;
if not (Model_parser.is_model_empty m) then begin
fprintf fmt "\nCounter-example model:";
Model_parser.print_model ~print_attrs fmt m
if json_model then
Model_parser.print_model ~print_attrs fmt m
else
Model_parser.print_model_human ?me_name_trans:None ~print_attrs fmt m
end;
if ans == HighFailure then
fprintf fmt "@\nProver exit status: %a@\nProver output:@\n%s@."
......
......@@ -52,7 +52,8 @@ type prover_result = {
val print_prover_answer : Format.formatter -> prover_answer -> unit
(** Pretty-print a {! prover_answer} *)
val print_prover_result : Format.formatter -> prover_result -> unit
val print_prover_result :
json_model:bool -> Format.formatter -> prover_result -> unit
(** Pretty-print a prover_result. The answer and the time are output.
The output of the prover is printed if and only if the answer is
a [HighFailure] *)
......
......@@ -41,7 +41,8 @@ let print_status fmt st =
| Scheduled -> fprintf fmt "Scheduled"
| Running -> fprintf fmt "Running"
| Done r ->
fprintf fmt "Done(%a)" Call_provers.print_prover_result r
fprintf fmt "Done(%a)"
(Call_provers.print_prover_result ~json_model:false) r
| Interrupted -> fprintf fmt "Interrupted"
| Detached -> fprintf fmt "Detached"
| InternalFailure e ->
......@@ -1035,8 +1036,8 @@ let print_report fmt (r: report) =
match r with
| Result (new_r, old_r) ->
Format.fprintf fmt "new_result = %a, old_result = %a@."
Call_provers.print_prover_result new_r
Call_provers.print_prover_result old_r
(Call_provers.print_prover_result ~json_model:false) new_r
(Call_provers.print_prover_result ~json_model:false) old_r
| CallFailed e ->
Format.fprintf fmt "Callfailed %a@." Exn_printer.exn_printer e
| Replay_interrupted ->
......@@ -1047,7 +1048,7 @@ let print_report fmt (r: report) =
Format.fprintf fmt "No edited file@."
| No_former_result new_r ->
Format.fprintf fmt "new_result = %a, no former result@."
Call_provers.print_prover_result new_r
(Call_provers.print_prover_result ~json_model:false) new_r
(* TODO to be removed when we have a better way to print *)
let replay_print fmt (lr: (proofNodeID * Whyconf.prover * Call_provers.resource_limit * report) list) =
......@@ -1227,7 +1228,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
| Done res ->
assert (res.Call_provers.pr_answer = Call_provers.Valid);
Debug.dprintf debug "Bisecting: %a.@."
Call_provers.print_prover_result res
(Call_provers.print_prover_result ~json_model:false) res
end
in
schedule_proof_attempt ?save_to:None c pn prover ~limit ~callback ~notification
......
......@@ -484,7 +484,8 @@ let print_proof_attempt fmt pa =
fprintf fmt "%a tl=%d %a"
Whyconf.print_prover pa.prover
pa.limit.Call_provers.limit_time
(Pp.print_option Call_provers.print_prover_result) pa.proof_state
(Pp.print_option (Call_provers.print_prover_result ~json_model:false))
pa.proof_state
let rec print_proof_node s (fmt: Format.formatter) p =
let pn = get_proofNode s p in
......
......@@ -26,6 +26,8 @@ let opt_input = ref None
let opt_theory = ref None
let opt_trans = ref []
let opt_metas = ref []
(* Option for printing counterexamples with JSON formatting *)
let opt_json = ref false
let add_opt_file x =
let tlist = Queue.create () in
......@@ -137,6 +139,8 @@ let option_list = [
"<dir> print the selected goals to separate files in <dir>";
"--output", Arg.String (fun s -> opt_output := Some s),
" same as -o";
"--json", Arg.Set opt_json,
" print counterexamples in JSON format";
"--print-theory", Arg.Set opt_print_theory,
" print selected theories";
"--print-namespace", Arg.Set opt_print_namespace,
......@@ -254,7 +258,7 @@ let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
let res = Call_provers.wait_on_call call in
printf "%s %s %s: %a@." fname tname
(task_goal task).Decl.pr_name.Ident.id_string
Call_provers.print_prover_result res;
(Call_provers.print_prover_result ~json_model:!opt_json) res;
if res.Call_provers.pr_answer <> Call_provers.Valid then unproved := true
| None, None ->
Driver.print_task drv std_formatter task
......
......@@ -118,7 +118,7 @@ let () =
if Debug.test_flag debug then
Printf.eprintf "Progress: %d/%d/%d \r%!" w s r)
let print_result = Call_provers.print_prover_result
let print_result = Call_provers.print_prover_result ~json_model:false
module S = Session_itp
......
......@@ -283,7 +283,9 @@ let print_proof_attempt fmt pa_id =
| None -> fprintf fmt "%s" pa.node_name
| Some _pr ->
fprintf fmt "%s %a"
pa.node_name (Pp.print_option Call_provers.print_prover_result) (get_result pa.node_proof)
pa.node_name
(Pp.print_option (Call_provers.print_prover_result ~json_model:false))
(get_result pa.node_proof)
let rec print_proof_node (fmt: Format.formatter) goal_id =
let goal = Hnode.find nodes goal_id in
......
......@@ -239,7 +239,8 @@ struct
let print_proof_status fmt = function
| None -> fprintf fmt "No result"
| Some res -> fprintf fmt "Done: %a" Call_provers.print_prover_result res
| Some res -> fprintf fmt "Done: %a"
(Call_provers.print_prover_result ~json_model:true) res
let print_proof_attempt s fmt pa =
let pa = get_proof_attempt_node s pa in
......
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