From 17ff54f17a364e74fed99544cc05a4a1ea9020ff Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 30 Oct 2018 16:25:43 -0700 Subject: [PATCH] Logging: increase/decrease indent Reviewed By: jeremydubreil Differential Revision: D12840641 fbshipit-source-id: faed7dfc7 --- infer/src/base/Logging.ml | 18 +++---- infer/src/base/Logging.mli | 4 +- infer/src/biabduction/Abs.ml | 4 +- infer/src/biabduction/Prover.ml | 78 ++++++++++++++--------------- infer/src/biabduction/Rearrange.ml | 16 +++--- infer/src/biabduction/Tabulation.ml | 12 ++--- infer/src/biabduction/interproc.ml | 48 +++++++++--------- infer/src/checkers/PulseDomain.ml | 4 +- 8 files changed, 91 insertions(+), 93 deletions(-) diff --git a/infer/src/base/Logging.ml b/infer/src/base/Logging.ml index 5b1e90f45..00be9724c 100644 --- a/infer/src/base/Logging.ml +++ b/infer/src/base/Logging.ml @@ -348,8 +348,8 @@ let setup_log_file () = (** delayable print action *) type print_action = - | PTdecrease_indent : int -> print_action - | PTincrease_indent : int -> print_action + | PTdecrease_indent : print_action + | PTincrease_indent : print_action | PTstr : {s: string; color: Pp.color option; ln: bool} -> print_action | PTwarning : string -> print_action | PTerror : string -> print_action @@ -377,12 +377,10 @@ let pp_maybe_with_color ?color pp fmt x = (** Execute the delayed print actions *) let force_delayed_print fmt = function - | PTdecrease_indent n -> - for _ = 1 to n do - F.fprintf fmt "@]" - done - | PTincrease_indent n -> - F.fprintf fmt "%s@[" (String.make (2 * n) ' ') + | PTdecrease_indent -> + F.pp_close_box fmt () + | PTincrease_indent -> + F.fprintf fmt " @[" | PTstr {s; color; ln} -> pp_maybe_with_color ?color F.pp_print_string fmt s ; if ln then F.pp_force_newline fmt () @@ -458,7 +456,7 @@ let d_indent indent = (** dump command to increase the indentation level *) -let d_increase_indent (indent : int) = add_print_action (PTincrease_indent indent) +let d_increase_indent () = add_print_action PTincrease_indent (** dump command to decrease the indentation level *) -let d_decrease_indent (indent : int) = add_print_action (PTdecrease_indent indent) +let d_decrease_indent () = add_print_action PTdecrease_indent diff --git a/infer/src/base/Logging.mli b/infer/src/base/Logging.mli index 01f4d81f4..c05f7341e 100644 --- a/infer/src/base/Logging.mli +++ b/infer/src/base/Logging.mli @@ -126,8 +126,8 @@ val d_info : string -> unit val d_indent : int -> unit (** dump an indentation *) -val d_increase_indent : int -> unit +val d_increase_indent : unit -> unit (** dump command to increase the indentation level *) -val d_decrease_indent : int -> unit +val d_decrease_indent : unit -> unit (** dump command to decrease the indentation level *) diff --git a/infer/src/biabduction/Abs.ml b/infer/src/biabduction/Abs.ml index 59bcc8913..ecbe321e1 100644 --- a/infer/src/biabduction/Abs.ml +++ b/infer/src/biabduction/Abs.ml @@ -1019,7 +1019,7 @@ let check_junk pname tenv prop = if should_remove_hpred entries then ( let part = if fp_part then "footprint" else "normal" in L.d_printfln ".... Prop with garbage in %s part ...." part ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; L.d_strln "PROP:" ; Prop.d_prop prop ; L.d_ln () ; @@ -1052,7 +1052,7 @@ let check_junk pname tenv prop = in List.iter ~f:do_entry entries ; !res in - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; let is_undefined = Option.value_map ~f:PredSymb.is_undef ~default:false alloc_attribute in diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml index cca9637df..3e0e73de5 100644 --- a/infer/src/biabduction/Prover.ml +++ b/infer/src/biabduction/Prover.ml @@ -15,7 +15,7 @@ module F = Format let decrease_indent_when_exception thunk = try thunk () with exn when SymOp.exn_not_failure exn -> - IExn.reraise_after exn ~f:(fun () -> L.d_decrease_indent 1) + IExn.reraise_after exn ~f:(fun () -> L.d_decrease_indent ()) let compute_max_from_nonempty_int_list l = uw (List.max_elt ~compare:IntLit.compare_value l) @@ -1212,9 +1212,9 @@ end = struct let d_missing_ sub = L.d_strln "SUB: " ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Prop.d_sub sub ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; if !missing_pi <> [] && !missing_sigma <> [] then ( L.d_ln () ; Prop.d_pi !missing_pi ; L.d_strln "*" ; Prop.d_sigma !missing_sigma ) else if !missing_pi <> [] then ( L.d_ln () ; Prop.d_pi !missing_pi ) @@ -1222,15 +1222,15 @@ end = struct if !missing_fld <> [] then ( L.d_ln () ; L.d_strln "MISSING FLD:" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Prop.d_sigma !missing_fld ; - L.d_decrease_indent 1 ) ; + L.d_decrease_indent () ) ; if !missing_typ <> [] then ( L.d_ln () ; L.d_strln "MISSING TYPING:" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; d_typings !missing_typ ; - L.d_decrease_indent 1 ) + L.d_decrease_indent () ) let d_missing sub = @@ -1246,10 +1246,10 @@ end = struct if !frame_fld <> [] then ( L.d_ln () ; L.d_strln "[FRAME FLD:" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Prop.d_sigma !frame_fld ; L.d_str "]" ; - L.d_decrease_indent 1 ) + L.d_decrease_indent () ) let d_frame_typ () = @@ -1257,19 +1257,19 @@ end = struct if !frame_typ <> [] then ( L.d_ln () ; L.d_strln "[FRAME TYPING:" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; d_typings !frame_typ ; L.d_str "]" ; - L.d_decrease_indent 1 ) + L.d_decrease_indent () ) (** Dump an implication *) let d_implication (sub1, sub2) (p1, p2) = let p1, p2 = (Prop.prop_sub sub1 p1, Prop.prop_sub sub2 p2) in L.d_strln "SUB:" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Prop.d_sub sub1 ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; Prop.d_prop p1 ; d_missing sub2 ; @@ -2114,14 +2114,14 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 let _, para_inst1 = Sil.hpara_instantiate para1 e1 n' elist1 in let hpred_list1 = para_inst1 @ [Prop.mk_lseg tenv Sil.Lseg_PE para1 n' f1 elist1] in let iter1'' = Prop.prop_iter_update_current_by_list iter1' hpred_list1 in - L.d_increase_indent 1 ; + L.d_increase_indent () ; let res = decrease_indent_when_exception (fun () -> hpred_imply tenv calc_index_frame calc_missing subs (Prop.prop_iter_to_prop tenv iter1'') sigma2 hpred2 ) in - L.d_decrease_indent 1 ; res + L.d_decrease_indent () ; res | Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _ when Exp.equal (Sil.exp_sub (fst subs) iF1) e2 -> (* Unroll dllseg forward *) @@ -2131,14 +2131,14 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 para_inst1 @ [Prop.mk_dllseg tenv Sil.Lseg_PE para1 n' iF1 oF1 iB1 elist1] in let iter1'' = Prop.prop_iter_update_current_by_list iter1' hpred_list1 in - L.d_increase_indent 1 ; + L.d_increase_indent () ; let res = decrease_indent_when_exception (fun () -> hpred_imply tenv calc_index_frame calc_missing subs (Prop.prop_iter_to_prop tenv iter1'') sigma2 hpred2 ) in - L.d_decrease_indent 1 ; res + L.d_decrease_indent () ; res | Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _ when Exp.equal (Sil.exp_sub (fst subs) iB1) e2 -> (* Unroll dllseg backward *) @@ -2148,14 +2148,14 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 para_inst1 @ [Prop.mk_dllseg tenv Sil.Lseg_PE para1 iF1 oB1 iB1 n' elist1] in let iter1'' = Prop.prop_iter_update_current_by_list iter1' hpred_list1 in - L.d_increase_indent 1 ; + L.d_increase_indent () ; let res = decrease_indent_when_exception (fun () -> hpred_imply tenv calc_index_frame calc_missing subs (Prop.prop_iter_to_prop tenv iter1'') sigma2 hpred2 ) in - L.d_decrease_indent 1 ; res + L.d_decrease_indent () ; res | _ -> assert false ) ) ) | Sil.Hlseg (k, para2, e2_, f2_, elist2_) -> ( @@ -2182,13 +2182,13 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 | None -> let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2_ in let _, para_inst2 = Sil.hpara_instantiate para2 e2 f2 elist2 in - L.d_increase_indent 1 ; + L.d_increase_indent () ; let res = decrease_indent_when_exception (fun () -> sigma_imply tenv calc_index_frame false subs prop1 para_inst2 ) in (* calc_missing is false as we're checking an instantiation of the original list *) - L.d_decrease_indent 1 ; res + L.d_decrease_indent () ; res | Some iter1' -> ( let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2_ in (* force instantiation of existentials *) @@ -2210,7 +2210,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 let hpred_list2 = para_inst2 @ [Prop.mk_lseg tenv Sil.Lseg_PE para2 n' f2_ elist2_] in - L.d_increase_indent 1 ; + L.d_increase_indent () ; let res = decrease_indent_when_exception (fun () -> try sigma_imply tenv calc_index_frame calc_missing subs prop1 hpred_list2 @@ -2219,7 +2219,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 let _, para_inst3 = Sil.hpara_instantiate para2 e2_ f2_ elist2 in sigma_imply tenv calc_index_frame calc_missing subs prop1 para_inst3 ) in - L.d_decrease_indent 1 ; res + L.d_decrease_indent () ; res | Sil.Hdllseg _ -> assert false ) ) ) | Sil.Hdllseg (Sil.Lseg_PE, _, _, _, _, _, _) -> @@ -2261,13 +2261,13 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 else assert false (* Only base case of rhs list considered for now *) in - L.d_increase_indent 1 ; + L.d_increase_indent () ; let res = decrease_indent_when_exception (fun () -> sigma_imply tenv calc_index_frame false subs prop1 para_inst2 ) in (* calc_missing is false as we're checking an instantiation of the original list *) - L.d_decrease_indent 1 ; res + L.d_decrease_indent () ; res | Some iter1' -> (* Only consider implications between identical listsegs for now *) let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2 in @@ -2376,12 +2376,12 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 * let normal_case hpred2' = let subs', prop1' = try - L.d_increase_indent 1 ; + L.d_increase_indent () ; let res = decrease_indent_when_exception (fun () -> hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2' ) in - L.d_decrease_indent 1 ; res + L.d_decrease_indent () ; res with IMPL_EXC _ when calc_missing -> ( match is_constant_string_class subs hpred2' with | Some (s, is_string) -> @@ -2409,12 +2409,12 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 * ProverState.add_missing_sigma [hpred2'] ; (subs', prop1) ) in - L.d_increase_indent 1 ; + L.d_increase_indent () ; let res = decrease_indent_when_exception (fun () -> sigma_imply tenv calc_index_frame calc_missing subs' prop1' sigma2' ) in - L.d_decrease_indent 1 ; res + L.d_decrease_indent () ; res in match hpred2 with | Sil.Hpointsto (e2_, se2, t) -> @@ -2548,26 +2548,26 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2 List.iter ~f:(fun a -> ProverState.add_bounds_check (ProverState.BCfrom_pre a)) pi2_bcheck ; L.d_strln "pre_check_pure_implication" ; L.d_strln "pi1:" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Prop.d_pi pi1 ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; L.d_strln "pi2:" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Prop.d_pi pi2 ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; if pi2_bcheck <> [] then ( L.d_str "pi2 bounds checks: " ; Prop.d_pi pi2_bcheck ; L.d_ln () ) ; L.d_strln "returns" ; L.d_strln "sub1:" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Prop.d_sub (fst subs) ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; L.d_strln "sub2:" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Prop.d_sub (snd subs) ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; let (sub1, sub2), frame_prop = sigma_imply tenv false calc_missing subs prop1 sigma2 in let pi1' = Prop.pi_sub sub1 pi1 in @@ -2579,9 +2579,9 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2 (* handle implicit bound checks, plus those from array_len_imply *) check_array_bounds tenv (sub1, sub2) prop_for_impl ; L.d_strln "Result of Abduction" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; d_impl (sub1, sub2) (prop1, prop2) ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; L.d_strln "returning TRUE" ; let frame = frame_prop.Prop.sigma in diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index 984274e3c..700d2d6bc 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -80,7 +80,7 @@ let bounds_check tenv pname prop len e = let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp (t : Typ.t) (off : Sil.offset list) inst : Sil.atom list * Sil.strexp * Typ.t = if Config.trace_rearrange then ( - L.d_increase_indent 1 ; + L.d_increase_indent () ; L.d_strln "entering create_struct_values" ; L.d_str "typ: " ; Typ.d_full t ; @@ -177,7 +177,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp let _, se, _ = res in L.d_strln "exiting create_struct_values, returning" ; Sil.d_sexp se ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; L.d_ln () ) ; res @@ -1101,7 +1101,7 @@ let pp_rearrangement_error message prop lexp = (** do re-arrangement for an iter whose current element is a pointsto *) let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst = if Config.trace_rearrange then ( - L.d_increase_indent 1 ; + L.d_increase_indent () ; L.d_strln "entering iter_rearrange_ptsto" ; L.d_str "lexp: " ; Sil.d_exp lexp ; @@ -1149,7 +1149,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst = if Config.trace_rearrange then ( L.d_strln "exiting iter_rearrange_ptsto, returning results" ; Prop.d_proplist_with_typ (List.map ~f:(Prop.prop_iter_to_prop tenv) res) ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; L.d_ln () ) ; res @@ -1361,12 +1361,12 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst : | Tstruct _ -> (* access through field: get the struct type from the field *) if Config.trace_rearrange then ( - L.d_increase_indent 1 ; + L.d_increase_indent () ; L.d_printfln "iter_rearrange: root of lexp accesses field %a" Typ.Fieldname.pp f ; L.d_str " struct type from field: " ; Typ.d_full fld_typ ; L.d_ln () ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ) ; fld_typ | _ -> @@ -1378,7 +1378,7 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst : in let typ = root_typ_of_offsets (Sil.exp_get_offsets lexp) in if Config.trace_rearrange then ( - L.d_increase_indent 1 ; + L.d_increase_indent () ; L.d_strln "entering iter_rearrange" ; L.d_str "lexp: " ; Sil.d_exp lexp ; @@ -1469,7 +1469,7 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst : if Config.trace_rearrange then ( L.d_strln "exiting iter_rearrange, returning results" ; Prop.d_proplist_with_typ (List.map ~f:(Prop.prop_iter_to_prop tenv) res) ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; L.d_ln () ) ; res diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index 4ccfa7afd..79423e967 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -864,7 +864,7 @@ let combine tenv ret_id (posts : ('a Prop.t * Paths.Path.t) list) actual_pre pat (Prop.prop_sub split.sub p, path) ) posts' in - L.d_increase_indent 1 ; + L.d_increase_indent () ; L.d_strln "New footprint:" ; Prop.d_pi_sigma split.missing_pi split.missing_sigma ; L.d_ln () ; @@ -885,7 +885,7 @@ let combine tenv ret_id (posts : ('a Prop.t * Paths.Path.t) list) actual_pre pat L.d_ln () ; L.d_strln "Instantiated post:" ; Propgraph.d_proplist Prop.prop_emp (List.map ~f:fst instantiated_post) ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; let compute_result post_p = let post_p' = @@ -1147,14 +1147,14 @@ let exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop let spec_pre = BiabductionSummary.Jprop.to_prop spec.BiabductionSummary.pre in L.d_printfln "EXECUTING SPEC %d/%d" n nspecs ; L.d_strln "ACTUAL PRECONDITION =" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Prop.d_prop actual_pre ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; L.d_strln "SPEC =" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; L.d_pp BiabductionSummary.pp_spec spec ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; SymOp.pay () ; (* pay one symop *) diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 334feaeae..9467eb7f2 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -215,36 +215,36 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t Propset.map tenv f pset in L.d_printfln "#### Extracted footprint of %a: ####" Typ.Procname.pp proc_name ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Propset.d Prop.prop_emp pset' ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; L.d_ln () ; let pset'' = collect_do_abstract_pre proc_name tenv pset' in let plist_meet = do_meet_pre tenv pset'' in L.d_printfln "#### Footprint of %a after Meet ####" Typ.Procname.pp proc_name ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Propgraph.d_proplist Prop.prop_emp plist_meet ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; L.d_ln () ; - L.d_increase_indent 2 ; + L.d_increase_indent () ; (* Indent for the join output *) let jplist = do_join_pre tenv plist_meet in - L.d_decrease_indent 2 ; + L.d_decrease_indent () ; L.d_ln () ; L.d_printfln "#### Footprint of %a after Join ####" Typ.Procname.pp proc_name ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; BiabductionSummary.Jprop.d_list ~shallow:false jplist ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; let jplist' = List.map ~f:(BiabductionSummary.Jprop.map (Prop.prop_rename_primed_footprint_vars tenv)) jplist in L.d_printfln "#### Renamed footprint of %a: ####" Typ.Procname.pp proc_name ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; BiabductionSummary.Jprop.d_list ~shallow:false jplist' ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; let jplist'' = let f p = @@ -253,9 +253,9 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t List.map ~f:(BiabductionSummary.Jprop.map f) jplist' in L.d_printfln "#### Abstracted footprint of %a: ####" Typ.Procname.pp proc_name ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; BiabductionSummary.Jprop.d_list ~shallow:false jplist'' ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; jplist'' @@ -444,7 +444,7 @@ let forward_tabulate summary exe_env tenv proc_cfg wl = in L.d_printfln "**** %s Node: %a, Procedure: %a, Session: %d, Todo: %d ****" (log_string pname) Procdesc.Node.pp curr_node Typ.Procname.pp pname session (Paths.PathSet.size pathset_todo) ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv pathset_todo) ; L.d_strln ".... Instructions: ...." ; Procdesc.Node.d_instrs ~sub_instrs:true (State.get_instr ()) curr_node ; @@ -453,20 +453,20 @@ let forward_tabulate summary exe_env tenv proc_cfg wl = in let do_prop (curr_node : ProcCfg.Exceptional.Node.t) handle_exn prop path cnt num_paths = L.d_printfln "Processing prop %d/%d" cnt num_paths ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; try State.reset_diverging_states_node () ; let pset = do_symbolic_execution exe_env summary proc_cfg handle_exn tenv curr_node prop path in propagate_nodes_divergence tenv proc_cfg pset curr_node wl ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () with exn -> IExn.reraise_if exn ~f:(fun () -> (not !BiabductionConfig.footprint) || not (Exceptions.handle_exception exn) ) ; handle_exn exn ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () in let do_node curr_node pathset_todo session handle_exn = @@ -670,9 +670,9 @@ let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * BiabductionSumma assert false in L.d_printfln "#### [FUNCTION %a] Postconditions after join ####" Typ.Procname.pp pname ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv (fst res)) ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; L.d_ln () ; res @@ -776,7 +776,7 @@ let execute_filter_prop summary exe_env tenv proc_cfg forward_tabulate summary exe_env tenv proc_cfg wl ; do_before_node 0 init_node ; L.d_printfln ~color:Green "#### Finished: RE-execution for %a ####" Typ.Procname.pp pname ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; L.d_strln "Precond:" ; Prop.d_prop (BiabductionSummary.Jprop.to_prop precondition) ; L.d_ln () ; @@ -800,16 +800,16 @@ let execute_filter_prop summary exe_env tenv proc_cfg BiabductionSummary.Jprop.Joined (n, p, jp1, jp2) in let spec = BiabductionSummary.{pre; posts; visited} in - L.d_decrease_indent 1 ; do_after_node init_node ; Some spec + L.d_decrease_indent () ; do_after_node init_node ; Some spec with RE_EXE_ERROR -> do_before_node 0 init_node ; Printer.force_delayed_prints () ; L.d_printfln ~color:Red "#### [FUNCTION %a] ...ERROR" Typ.Procname.pp pname ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; L.d_strln "when starting from pre:" ; Prop.d_prop (BiabductionSummary.Jprop.to_prop precondition) ; L.d_strln "This precondition is filtered out." ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; do_after_node init_node ; None @@ -846,12 +846,12 @@ let perform_analysis_phase exe_env tenv (summary : Summary.t) (proc_cfg : ProcCf in Propset.fold add Paths.PathSet.empty init_props in - L.d_increase_indent 1 ; + L.d_increase_indent () ; L.d_strln "initial props =" ; Propset.d Prop.prop_emp init_props ; L.d_ln () ; L.d_ln () ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; Worklist.add wl start_node ; ignore (path_set_put_todo wl start_node init_edgeset) ; forward_tabulate summary exe_env tenv proc_cfg wl diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 5a5bb2971..916e1b333 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -306,13 +306,13 @@ module Domain : AbstractDomain.S with type astate = t = struct in if has_converged then ( L.d_strln "Join unified addresses:" ; - L.d_increase_indent 1 ; + L.d_increase_indent () ; Container.iter state.subst ~fold:AddressUF.fold_sets ~f:(fun ((repr : AddressUF.Repr.t), set) -> L.d_printfln "%a=%a" AbstractAddress.pp (repr :> AbstractAddress.t) AddressUnionSet.pp set ) ; - L.d_decrease_indent 1 ; + L.d_decrease_indent () ; let stack = AliasingDomain.map (to_canonical_address state.subst) state.astate.stack in let invalids = InvalidAddressesDomain.map (to_canonical_address state.subst) state.astate.invalids