Commit d0925705 authored by Francois Bobot's avatar Francois Bobot

Debug : use references and add dprintf

parent 7ca93801
......@@ -59,7 +59,10 @@ let rec grep out l = match l with
| HighFailure -> assert false
with Not_found -> grep out l end
let call_prover debug command opt_cout buffer =
let debug = Debug.register_flag "call_prover"
let call_prover command opt_cout buffer =
let time = Unix.gettimeofday () in
let (cin,_) as p = match opt_cout with
| Some cout ->
......@@ -73,14 +76,11 @@ let call_prover debug command opt_cout buffer =
let out = channel_contents cin in
let ret = Unix.close_process p in
let time = Unix.gettimeofday () -. time in
if debug then eprintf "Call_provers: prover output:@\n%s@." out;
Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
ret, out, time
let debug = Debug.register_flag "call_prover"
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
~regexps ~exitcodes ~filename buffer () =
let debug = Debug.test_flag debug in
let on_stdin = ref true in
let on_timelimit = ref false in
let cmd_regexp = Str.regexp "%\\(.\\)" in
......@@ -93,28 +93,28 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
in
let cmd = Str.global_substitute cmd_regexp (replace "") command in
let ret, out, time =
if !on_stdin then call_prover debug cmd None buffer else begin
if !on_stdin then call_prover cmd None buffer else begin
let fout,cout = Filename.open_temp_file "why_" ("_" ^ filename) in
try
let cmd = Str.global_substitute cmd_regexp (replace fout) command in
let res = call_prover debug cmd (Some cout) buffer in
if not debug then Sys.remove fout;
let res = call_prover cmd (Some cout) buffer in
if Debug.nottest_flag debug then Sys.remove fout;
res
with e ->
close_out cout;
if not debug then Sys.remove fout;
if Debug.nottest_flag debug then Sys.remove fout;
raise e
end
in
let ans = match ret with
| Unix.WSTOPPED n ->
if debug then eprintf "Call_provers: stopped by signal %d@." n;
Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
HighFailure
| Unix.WSIGNALED n ->
if debug then eprintf "Call_provers: killed by signal %d@." n;
Debug.dprintf debug "Call_provers: killed by signal %d@." n;
HighFailure
| Unix.WEXITED n ->
if debug then eprintf "Call_provers: exited with status %d@." n;
Debug.dprintf debug "Call_provers: exited with status %d@." n;
(try List.assoc n exitcodes with Not_found -> grep out regexps)
in
let ans = match ans with
......
......@@ -1194,9 +1194,8 @@ let decl env gl = function
Pgm_env.logic_decls dl env gl, []
| Pgm_ptree.Dlet (id, e) ->
let e = type_expr gl e in
if Debug.test_flag debug then
eprintf "@[--typing %s-----@\n %a@\n%a@]@."
id.id print_expr e print_type_v e.expr_type_v;
Debug.dprintf debug "@[--typing %s-----@\n %a@\n%a@]@."
id.id print_expr e print_type_v e.expr_type_v;
let ls, gl = add_global id.id_loc id.id e.expr_type_v gl in
gl, [Dlet (ls, e)]
| Pgm_ptree.Dletrec dl ->
......
......@@ -388,19 +388,16 @@ let add_wp_decl l f env =
let decl env = function
| Pgm_ttree.Dlet (ls, e) ->
if Debug.test_flag debug then
eprintf "@[--effect %a-----@\n %a@]@\n----------------@."
Debug.dprintf debug "@[--effect %a-----@\n %a@]@\n----------------@."
Pretty.print_ls ls print_type_v e.expr_type_v;
let f = wp env e in
if Debug.test_flag debug then
eprintf "wp = %a@\n----------------@." Pretty.print_fmla f;
Debug.dprintf debug "wp = %a@\n----------------@." Pretty.print_fmla f;
let env = add_wp_decl ls f env in
env
| Pgm_ttree.Dletrec dl ->
let add_one env (ls, def) =
let f = wp_recfun env def in
if Debug.test_flag debug then
eprintf "wp %a = %a@\n----------------@."
Debug.dprintf debug "wp %a = %a@\n----------------@."
print_ls ls Pretty.print_fmla f;
add_wp_decl ls f env
in
......
......@@ -17,30 +17,33 @@
(* *)
(**************************************************************************)
let on = ref 0
let formatter = ref Format.err_formatter
exception UnknownFlag of string
type flag = string
type flag = bool ref
let flag_table = Hashtbl.create 17
let register_flag s = Hashtbl.replace flag_table s false; s
let register_flag s =
try
Hashtbl.find flag_table s
with Not_found ->
let flag = ref false in
Hashtbl.replace flag_table s flag;
flag
let lookup_flag s =
if Hashtbl.mem flag_table s then s else raise (UnknownFlag s)
try Hashtbl.find flag_table s with Not_found -> raise (UnknownFlag s)
let list_flags () = Hashtbl.fold (fun s v acc -> (s,s,v)::acc) flag_table []
let list_flags () = Hashtbl.fold (fun s v acc -> (s,v,!v)::acc) flag_table []
let test_flag s = !on > 0 && Hashtbl.find flag_table s
let test_flag s = !s
let nottest_flag s = !s
let raw_set_flag s = Hashtbl.replace flag_table s true
let raw_unset_flag s = Hashtbl.replace flag_table s false
let set_flag s = if not (test_flag s) then (raw_set_flag s; incr on)
let unset_flag s = if test_flag s then (raw_unset_flag s; decr on)
let toggle_flag s = if test_flag s
then (raw_unset_flag s; decr on) else (raw_set_flag s; incr on)
let set_flag s = s := true
let unset_flag s = s := false
let toggle_flag s = s := not !s
let () = Exn_printer.register (fun fmt e -> match e with
| UnknownFlag s -> Format.fprintf fmt "unknown debug flag `%s'@." s
......@@ -48,3 +51,7 @@ let () = Exn_printer.register (fun fmt e -> match e with
let stack_trace = register_flag "stack_trace"
let set_debug_formatter = (:=) formatter
let dprintf flag =
if !flag then Format.fprintf !formatter else Format.ifprintf !formatter
......@@ -18,15 +18,30 @@
(**************************************************************************)
type flag
(* Flag used for debugging only part of Why *)
val register_flag : string -> flag
(** Register a new flag. If someone try to register two times the same
flag the same one is used *)
val lookup_flag : string -> flag
val list_flags : unit -> (string * flag * bool) list
(** List the known flags *)
(** Modify the state of a flag *)
val set_flag : flag -> unit
val unset_flag : flag -> unit
val toggle_flag : flag -> unit
val test_flag : flag -> bool
(** Return the state of the flag *)
val nottest_flag : flag -> bool
val set_debug_formatter : Format.formatter -> unit
(** Set the formatter used when printing debug material *)
val dprintf : flag -> ('a, Format.formatter, unit) format -> 'a
(** Print only if the flag is set *)
val stack_trace : flag
(** stack_trace flag *)
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