Commit 8d66bf6d authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

debug option print_locs also prints locs of terms and formulas

parent f04b1942
......@@ -204,7 +204,10 @@ let print_ident_labels fmt id =
else ()
let rec print_term fmt t = print_lterm 0 fmt t
let rec print_term fmt t =
if Debug.test_flag debug_print_locs then
Util.option_iter (fun l -> fprintf fmt "%a " print_loc l) t.t_loc;
print_lterm 0 fmt t
and print_lterm pri fmt t = match t.t_label with
| _ when Debug.nottest_flag debug_print_labels
......
......@@ -601,7 +601,11 @@ and wp_desc env rm e q = match e.expr_desc with
| Eassert (Ptree.Aassert, f) ->
let (_, q), _ = q in
wp_and (wp_expl "assertion" f) q
let f = wp_expl "assertion" f in
(* eprintf "assert: AVANT f = %a@." print_term f; *)
let f = wp_and f q in
(* eprintf "assert: APRES f = %a@." print_term f; *)
f
| Eassert (Ptree.Acheck, f) ->
let (_, q), _ = q in
wp_and ~sym:true (wp_expl "check" f) q
......
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