Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 4e7deccb authored by MARCHE Claude's avatar MARCHE Claude

make debug flags systematically print their own name

parent d9189143
......@@ -213,7 +213,7 @@ let load_config config original_config =
}
let save_config t =
Debug.dprintf debug "[GUI config] saving IDE config file@.";
Debug.dprintf debug "[config] saving IDE config file@.";
(* taking original config, without the extra_config *)
let config = t.original_config in
(* copy possibly modified settings to original config *)
......@@ -501,7 +501,7 @@ let resize_images size =
()
let init () =
Debug.dprintf debug "[GUI config] reading icons...@?";
Debug.dprintf debug "[config] reading icons...@?";
load_icon_names ();
why_icon := image "logo-why";
resize_images 20;
......@@ -1135,7 +1135,7 @@ let run_auto_detection gconfig =
()
*)
(*let () = Debug.dprintf debug "[GUI config] end of configuration initialization@."*)
(*let () = Debug.dprintf debug "[config] end of configuration initialization@."*)
(*
let uninstalled_prover c eS unknown =
......
......@@ -61,14 +61,14 @@ module Protocol_why3ide = struct
~desc:"Print@ debugging@ messages@ about@ Why3Ide@ protocol@"
let print_request_debug r =
Debug.dprintf debug_proto "[IDE proto] request %a@." print_request r;
Debug.dprintf debug_proto "request %a@." print_request r;
Debug.dprintf debug_json "%a@." print_request_json r
let print_msg_debug m =
Debug.dprintf debug_proto "[IDE proto] message %a@." print_msg m
Debug.dprintf debug_proto "message %a@." print_msg m
let print_notify_debug n =
Debug.dprintf debug_proto "[IDE proto] handling notification %a@." print_notify n;
Debug.dprintf debug_proto "handling notification %a@." print_notify n;
Debug.dprintf debug_json "%a@." print_notification_json n
let list_requests: ide_request list ref = ref []
......@@ -76,7 +76,7 @@ module Protocol_why3ide = struct
let get_requests () =
let n = List.length !list_requests in
if n > 0 then
Debug.dprintf debug_proto "[IDE proto] got %d new requests@." n;
Debug.dprintf debug_proto "got %d new requests@." n;
let l = List.rev !list_requests in
list_requests := [];
l
......@@ -95,7 +95,7 @@ module Protocol_why3ide = struct
let get_notified () =
let n = List.length !notification_list in
if n > 0 then
Debug.dprintf debug_proto "[IDE proto] got %d new notifications@." n;
Debug.dprintf debug_proto "got %d new notifications@." n;
let l = List.rev !notification_list in
notification_list := [];
l
......@@ -207,7 +207,7 @@ let () =
Queue.iter (fun f -> send_request (Add_file_req f)) files
let () =
Debug.dprintf debug "[GUI] Init the GTK interface...@?";
Debug.dprintf debug "Init the GTK interface...@?";
ignore (GtkMain.Main.init ());
Debug.dprintf debug " done.@.";
Gconfig.init ()
......@@ -631,7 +631,7 @@ let view_time_column =
v
let goals_model,goals_view =
Debug.dprintf debug "[GUI] Creating tree model...@?";
Debug.dprintf debug "Creating tree model...@?";
let model = GTree.tree_store cols in
let view = GTree.view ~model ~packing:scrolled_session_view#add () in
let () = view#selection#set_mode (* `SINGLE *) `MULTIPLE in
......@@ -642,7 +642,7 @@ let goals_model,goals_view =
let _: int = view#append_column view_name_column in
let _: int = view#append_column view_status_column in
let _: int = view#append_column view_time_column in
Debug.dprintf debug "[GTK IDE] done@.";
Debug.dprintf debug "done@.";
model,view
......@@ -954,7 +954,7 @@ let _ =
let () =
let n = gconfig.session_nb_processes in
Debug.dprintf debug "[IDE] setting max proof tasks to %d@." n;
Debug.dprintf debug "setting max proof tasks to %d@." n;
send_request (Set_max_tasks_req n)
(********************)
......@@ -1180,7 +1180,7 @@ let on_selected_row r =
let (_ : GtkSignal.id) =
goals_view#selection#connect#after#changed ~callback:
(fun () ->
Debug.dprintf debug "[IDE INFO] running callback of goals_view#selection#connect#after#changed@.";
Debug.dprintf debug "running callback of goals_view#selection#connect#after#changed@.";
begin
match get_selected_row_references () with
| [r] -> on_selected_row r;
......@@ -1190,17 +1190,17 @@ let (_ : GtkSignal.id) =
let (_ : GtkSignal.id) =
let callback ev =
Debug.dprintf debug "[IDE INFO] running callback of goals_view#event#connect#button_press@.";
Debug.dprintf debug "running callback of goals_view#event#connect#button_press@.";
let n = GdkEvent.Button.button ev in
begin
Debug.dprintf debug "[IDE INFO] button number %d was clicked on the tree view@." n;
Debug.dprintf debug "button number %d was clicked on the tree view@." n;
match n with
| 1 -> (* Left click *) false
| 2 -> (* Middle click *) false
| 3 -> (* Right click *)
Debug.dprintf debug "[IDE INFO] before tools_menu#popup@.";
Debug.dprintf debug "before tools_menu#popup@.";
tools_menu#popup ~button:3 ~time:(GdkEvent.Button.time ev);
Debug.dprintf debug "[IDE INFO] after tools_menu#popup@.";
Debug.dprintf debug "after tools_menu#popup@.";
true
| _ -> (* Error case TODO *) assert false
end
......@@ -1572,7 +1572,7 @@ let add_submenu_strategy (shortcut,strategy) =
Opt.iter (fun (_,key,modi) -> i#add_accelerator ~group:tools_accel_group ~modi key)
(parse_shortcut_as_key shortcut);
let callback () =
Debug.dprintf debug "[IDE INFO] interp command '%s'@." shortcut;
Debug.dprintf debug "interp command '%s'@." shortcut;
interp shortcut
in
connect_menu_item i ~callback
......@@ -1586,7 +1586,7 @@ let add_submenu_prover (shortcut,prover_name,prover_parseable_name) =
Opt.iter (fun (_,key,modi) -> i#add_accelerator ~group:tools_accel_group ~modi key)
(parse_shortcut_as_key shortcut);
let callback () =
Debug.dprintf debug "[IDE INFO] interp command '%s'@." prover_parseable_name;
Debug.dprintf debug "interp command '%s'@." prover_parseable_name;
interp prover_parseable_name
in
connect_menu_item i ~callback
......
......@@ -388,7 +388,7 @@ let () =
let get_server_data () =
match !server_data with
| None ->
Format.eprintf "[ITP server] not yet initialized@.";
Format.eprintf "not yet initialized@.";
exit 1
| Some x -> x
......@@ -669,7 +669,7 @@ end
let main = Whyconf.get_main config in
let d = "why3_itp" in
let d = Whyconf.load_driver main env d [] in
Debug.dprintf debug "[ITP server] driver for task printing loaded@.";
Debug.dprintf debug "driver for task printing loaded@.";
d
with e ->
Format.eprintf "Fatal error while loading itp driver: %a@." Exn_printer.exn_printer e;
......@@ -960,9 +960,9 @@ end
(* ------------ init server ------------ *)
let init_server ?(send_source=true) config env f =
Debug.dprintf debug "[ITP server] loading session %s@." f;
Debug.dprintf debug "loading session %s@." f;
let ses,use_shapes = Session_itp.load_session f in
Debug.dprintf debug "[ITP server] creating controller@.";
Debug.dprintf debug "creating controller@.";
let c = create_controller config env ses in
(* let task_driver = task_driver config env in*)
server_data := Some
......@@ -999,9 +999,9 @@ end
Hstr.fold (fun c _ acc -> c :: acc) commands_table []
}
in
Debug.dprintf debug "[ITP server] sending initialization infos@.";
Debug.dprintf debug "sending initialization infos@.";
P.notify (Initialized infos);
Debug.dprintf debug "[ITP server] reloading source files@.";
Debug.dprintf debug "reloading source files@.";
let b = reload_files d.cont ~use_shapes in
if b then
begin
......
......@@ -68,7 +68,7 @@ rule xml_prolog fixattrs = parse
| "<?xml" space+ "version=\"1.0\"" space+ "encoding=\"UTF-8\"" space+ "?>"
{ xml_doctype fixattrs "1.0" "" lexbuf }
| "<?xml" ([^'?']|'?'[^'>'])* "?>"
{ Debug.dprintf debug "[Xml warning] prolog ignored@.";
{ Debug.dprintf debug "prolog ignored@.";
xml_doctype fixattrs "1.0" "" lexbuf }
| _
{ parse_error "wrong prolog" }
......@@ -99,25 +99,25 @@ and elements fixattrs group_stack element_stack = parse
{ match group_stack with
| [] ->
Debug.dprintf debug
"[Xml warning] unexpected closing Xml element `%s'@."
"unexpected closing Xml element `%s'@."
celem;
elements fixattrs group_stack element_stack lexbuf
| (elem,att,stack)::g ->
if celem <> elem then
Debug.dprintf debug
"[Xml warning] Xml element `%s' closed by `%s'@."
"Xml element `%s' closed by `%s'@."
elem celem;
let e = mk_element elem att element_stack in
elements fixattrs g (e::stack) lexbuf
}
| '<'
{ Debug.dprintf debug "[Xml warning] unexpected '<'@.";
{ Debug.dprintf debug "unexpected '<'@.";
elements fixattrs group_stack element_stack lexbuf }
| eof
{ match group_stack with
| [] -> element_stack
| (elem,_,_)::_ ->
Debug.dprintf debug "[Xml warning] unclosed Xml element `%s'@." elem;
Debug.dprintf debug "unclosed Xml element `%s'@." elem;
pop_all group_stack element_stack
}
| _ as c
......
......@@ -54,18 +54,18 @@ let check_ls ign_ls ls =
(Ty.oty_cons ls.Term.ls_args ls.Term.ls_value)
let detect_polymorphism_in_decl ign_ts ign_ls ign_pr d =
Debug.dprintf debug "[detect_polymorphism] |sts|=%d |sls|=%d |spr|=%d@."
Debug.dprintf debug "|sts|=%d |sls|=%d |spr|=%d@."
(Ty.Sts.cardinal ign_ts)
(Term.Sls.cardinal ign_ls)
(Spr.cardinal ign_pr);
Debug.dprintf debug "[detect_polymorphism] decl %a@."
Debug.dprintf debug "decl %a@."
Pretty.print_decl d;
match d.d_node with
| Dtype ts -> check_ts ign_ts ts
| Ddata dl ->
List.fold_left (fun acc (ts,_) -> acc || check_ts ign_ts ts) false dl
| Dparam ls ->
Debug.dprintf debug "[detect_polymorphism] param %a@."
Debug.dprintf debug "param %a@."
Pretty.print_ls ls;
check_ls ign_ls ls
| Dlogic dl ->
......
......@@ -13,7 +13,8 @@ let formatter = ref Format.err_formatter
exception UnknownFlag of string
type flag = bool ref
type flag = { flag_name : string;
mutable flag_value : bool }
let flag_table = Hashtbl.create 17
......@@ -25,7 +26,7 @@ let gen_register_flag (desc : Pp.formatted) s info =
try
fst3 (Hashtbl.find flag_table s)
with Not_found ->
let flag = ref false in
let flag = { flag_name = s; flag_value = false } in
Hashtbl.replace flag_table s (flag,info,desc);
flag
......@@ -33,7 +34,7 @@ let register_info_flag ~desc s = gen_register_flag desc s true
let register_flag ~desc s = gen_register_flag desc s false
let list_flags () =
Hashtbl.fold (fun s (v,_,desc) acc -> (s,v,!v,desc)::acc) flag_table []
Hashtbl.fold (fun s (v,_,desc) acc -> (s,v,v.flag_value,desc)::acc) flag_table []
let lookup_flag s =
try fst3 (Hashtbl.find flag_table s) with Not_found -> raise (UnknownFlag s)
......@@ -44,12 +45,12 @@ let is_info_flag s =
let flag_desc s =
try thd3 (Hashtbl.find flag_table s) with Not_found -> raise (UnknownFlag s)
let test_flag s = !s
let test_noflag s = not !s
let test_flag s = s.flag_value
let test_noflag s = not s.flag_value
let set_flag s = s := true
let unset_flag s = s := false
let toggle_flag s = s := not !s
let set_flag s = s.flag_value <- true
let unset_flag s = s.flag_value <- false
let toggle_flag s = s.flag_value <- not s.flag_value
let () = Exn_printer.register (fun fmt e -> match e with
| UnknownFlag s -> Format.fprintf fmt "unknown debug flag `%s'@." s
......@@ -76,10 +77,11 @@ let get_debug_formatter () = !formatter
let () = set_debug_formatter Format.err_formatter
let dprintf flag s =
if !flag then
if flag.flag_value then
begin
if !timestamp then Format.fprintf !formatter "<%f>"
(Unix.gettimeofday () -. time_start);
if timestamp.flag_value then Format.fprintf !formatter "<%f,%s>"
(Unix.gettimeofday () -. time_start) flag.flag_name
else Format.fprintf !formatter "<%s>" flag.flag_name;
Format.fprintf !formatter s
end
else Format.ifprintf !formatter s
......
......@@ -14,6 +14,7 @@ let create = String.create
let copy = String.copy
let set = String.set
let lowercase = String.lowercase
let capitalize = String.capitalize
let uncapitalize = String.uncapitalize
......
......@@ -319,7 +319,7 @@ let rec value_equality v1 v2 =
let eval_equ _ls l =
(*
eprintf "[interp] eval_equ ? @.";
eprintf "eval_equ ? @.";
*)
let res =
match l with
......@@ -331,7 +331,7 @@ let eval_equ _ls l =
| _ -> assert false
in
(*
Format.eprintf "[interp] eval_equ: OK@.";
Format.eprintf "eval_equ: OK@.";
*)
res
......@@ -690,7 +690,7 @@ let exec_array_get _env s _vty args =
let t = eval_map_get !ls_map_get [m;Vnum i] in
(*
eprintf
"[interp] exec_array_get (on reg %a)@ state =@ %a@ t[%a] -> %a@."
"exec_array_get (on reg %a)@ state =@ %a@ t[%a] -> %a@."
Mlw_pretty.print_reg r print_state s print_value (Vnum i) print_value t;
*)
Normal t,s
......@@ -698,7 +698,7 @@ let exec_array_get _env s _vty args =
(*
let t = eval_map_get !ls_map_get [m;Vnum i] in
eprintf
"[interp] exec_array_get (on map %a)@ state =@ %a@ t[%a] -> %a@."
"exec_array_get (on map %a)@ state =@ %a@ t[%a] -> %a@."
print_value m print_state s print_value (Vnum i) print_value t;
Normal t,s
*)
......@@ -730,7 +730,7 @@ let exec_array_set _env s _vty args =
let m = Mreg.find r s in
(*
eprintf
"[interp] exec_array_set (on reg %a)@ state =@ %a@ t[%a] -> %a@."
"exec_array_set (on reg %a)@ state =@ %a@ t[%a] -> %a@."
Mlw_pretty.print_reg r print_state s print_value i print_value t;
*)
let t = eval_map_set !ls_map_set [m;i;v] in
......@@ -747,7 +747,7 @@ let exec_array_set _env s _vty args =
with Not_found -> reg
in
let s' = Mreg.add reg t s in
eprintf "[interp] t[%a] <- %a (state = %a)@."
eprintf "t[%a] <- %a (state = %a)@."
print_value i print_value v print_state s';
Normal Vvoid,s'
*)
......@@ -892,7 +892,7 @@ and eval_match env s u tbl =
let rec iter tbl =
match tbl with
| [] ->
eprintf "[Exec] fatal error: pattern matching not exhaustive in evaluation.@.";
eprintf "fatal error: pattern matching not exhaustive in evaluation.@.";
assert false
| b::rem ->
let p,t = t_open_branch b in
......@@ -954,7 +954,7 @@ and eval_app env s ls tl =
in iter dl
| _ -> Vapp(ls,tl)
with Not_found ->
Format.eprintf "[Exec] definition of logic symbol %s not found@."
Format.eprintf "definition of logic symbol %s not found@."
ls.ls_name.Ident.id_string;
Vapp(ls,tl)
......@@ -1125,7 +1125,7 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
| Eif(e1,e2,e3) ->
begin
(*
eprintf "[interp] condition of the if : @?";
eprintf "condition of the if : @?";
*)
match eval_expr env s e1 with
| Normal t, s' ->
......@@ -1136,7 +1136,7 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
| _ ->
begin
eprintf
"@[[Exec] Cannot decide condition of if: @[%a@]@]@."
"@[Cannot decide condition of if: @[%a@]@]@."
print_value t;
Irred e, s
end
......@@ -1184,7 +1184,7 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
| DownTo -> BigInt.ge, BigInt.pred
in
let rec iter i s =
Debug.dprintf debug "[interp] for loop with index = %s@."
Debug.dprintf debug "for loop with index = %s@."
(BigInt.to_string i);
if le i b then
let env' = bind_vs pvs.pv_vs (Vnum i) env in
......@@ -1258,7 +1258,7 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
| Eany _
| Eabstr _
| Eabsurd ->
eprintf "@[[Exec] unsupported expression: @[%a@]@]@."
eprintf "@[unsupported expression: @[%a@]@]@."
(if Debug.test_flag debug then p_expr else Mlw_pretty.print_expr) e;
Irred e, s
......@@ -1266,7 +1266,7 @@ and exec_match env t s ebl =
let rec iter ebl =
match ebl with
| [] ->
eprintf "[Exec] Pattern matching not exhaustive in evaluation@.";
eprintf "Pattern matching not exhaustive in evaluation@.";
assert false
| (p,e)::rem ->
try
......@@ -1314,7 +1314,7 @@ and exec_app env s ps args (*spec*) ity_result =
try
Hps.find builtin_progs ps
with Not_found ->
eprintf "[Exec] definition of psymbol %s not found@."
eprintf "definition of psymbol %s not found@."
ps.ps_name.Ident.id_string;
raise CannotCompute
in
......@@ -1335,7 +1335,7 @@ and exec_app env s ps args (*spec*) ity_result =
let eval_global_expr env mkm tkm _writes e =
(*
eprintf "@[<hov 2>[interp] eval_global_expr:@ %a@]@."
eprintf "@[<hov 2>eval_global_expr:@ %a@]@."
p_expr e;
*)
get_builtins env;
......
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