From 4c0e217410a9920ca5af6bbfc767e6a6e830ff94 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 11 Sep 2018 02:09:42 -0700 Subject: [PATCH] Remove dead Config.pp_simple Reviewed By: jeremydubreil Differential Revision: D9751480 fbshipit-source-id: 1aa91b760 --- infer/src/IR/Pvar.ml | 20 ++++++-------- infer/src/backend/InferPrint.ml | 3 --- infer/src/backend/dotty.ml | 10 ++----- infer/src/base/Config.ml | 3 --- infer/src/base/Config.mli | 2 -- infer/src/biabduction/Prop.ml | 47 ++++++++++----------------------- 6 files changed, 24 insertions(+), 61 deletions(-) diff --git a/infer/src/IR/Pvar.ml b/infer/src/IR/Pvar.ml index 8c1e183d4..2b8c35840 100644 --- a/infer/src/IR/Pvar.ml +++ b/infer/src/IR/Pvar.ml @@ -66,18 +66,14 @@ let pp_translation_unit fmt = function None -> () | Some fname -> SourceFile.pp let pp_ f pv = let name = pv.pv_name in match pv.pv_kind with - | Local_var n -> - if !Config.pp_simple then Mangled.pp f name - else F.fprintf f "%a$%a" Typ.Procname.pp n Mangled.pp name - | Callee_var n -> - if !Config.pp_simple then F.fprintf f "%a|callee" Mangled.pp name - else F.fprintf f "%a$%a|callee" Typ.Procname.pp n Mangled.pp name - | Abduced_retvar (n, l) -> - if !Config.pp_simple then F.fprintf f "%a|abducedRetvar" Mangled.pp name - else F.fprintf f "%a$[%a]%a|abducedRetvar" Typ.Procname.pp n Location.pp l Mangled.pp name - | Abduced_ref_param (n, index, l) -> - if !Config.pp_simple then F.fprintf f "%a|abducedRefParam%d" Mangled.pp name index - else F.fprintf f "%a$[%a]%a|abducedRefParam" Typ.Procname.pp n Location.pp l Mangled.pp name + | Local_var _ -> + Mangled.pp f name + | Callee_var _ -> + F.fprintf f "%a|callee" Mangled.pp name + | Abduced_retvar _ -> + F.fprintf f "%a|abducedRetvar" Mangled.pp name + | Abduced_ref_param (_, index, _) -> + F.fprintf f "%a|abducedRefParam%d" Mangled.pp name index | Global_var (translation_unit, is_const, is_pod, _, _) -> F.fprintf f "#GB<%a%s%s>$%a" pp_translation_unit translation_unit (if is_const then "|const" else "") diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index da59af690..48cead321 100644 --- a/infer/src/backend/InferPrint.ml +++ b/infer/src/backend/InferPrint.ml @@ -919,14 +919,11 @@ let process_summary filters formats_by_report_kind linereader stats summary issu let file = (Summary.get_loc summary).Location.file in let proc_name = Summary.get_proc_name summary in let error_filter = error_filter filters proc_name in - let pp_simple_saved = !Config.pp_simple in - Config.pp_simple := true ; let issues_acc' = pp_summary_by_report_kind formats_by_report_kind summary error_filter linereader stats file issues_acc in if Config.precondition_stats then PreconditionStats.do_summary proc_name summary ; - Config.pp_simple := pp_simple_saved ; issues_acc' diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index e9e760687..74ae82db0 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -1207,8 +1207,6 @@ let print_icfg_dotty source cfg = (** Dotty printing for specs *) let pp_speclist_dotty f (splist : Prop.normal BiabductionSummary.spec list) = - let pp_simple_saved = !Config.pp_simple in - Config.pp_simple := true ; reset_proposition_counter () ; reset_dotty_spec_counter () ; F.fprintf f "@\n@\n@\ndigraph main { @\nnode [shape=box]; @\n" ; @@ -1220,18 +1218,14 @@ let pp_speclist_dotty f (splist : Prop.normal BiabductionSummary.spec list) = (BiabductionSummary.Jprop.to_prop s.BiabductionSummary.pre) s.BiabductionSummary.posts ) splist ; - F.fprintf f "@\n}" ; - Config.pp_simple := pp_simple_saved + F.fprintf f "@\n}" let pp_speclist_to_file (filename : DB.filename) spec_list = - let pp_simple_saved = !Config.pp_simple in - Config.pp_simple := true ; let outc = Out_channel.create (DB.filename_to_string (DB.filename_add_suffix filename ".dot")) in let fmt = F.formatter_of_out_channel outc in let () = F.fprintf fmt "#### Dotty version: ####@\n%a@\n@\n" pp_speclist_dotty spec_list in - Out_channel.close outc ; - Config.pp_simple := pp_simple_saved + Out_channel.close outc let pp_speclist_dotty_file (filename : DB.filename) spec_list = diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index cbd3ca6e3..cfd2cbbae 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -3029,9 +3029,6 @@ let run_in_footprint_mode f x = set_reference_and_call_function footprint true f let run_in_re_execution_mode f x = set_reference_and_call_function footprint false f x -(** if true, user simple pretty printing *) -let pp_simple = ref true - let reset_abs_val () = abs_val := abs_val_orig let run_with_abs_val_equal_zero f x = set_reference_and_call_function abs_val 0 f x diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index f978ef63e..262c4271d 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -680,8 +680,6 @@ val run_in_re_execution_mode : ('a -> 'b) -> 'a -> 'b (** Call f x with footprint set to false. Restore the initial value of footprint also in case of exception. *) -val pp_simple : bool ref - (** {2 Global variables with initial values specified by command-line options} *) val abs_val : int ref diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml index 92c811f2d..028b0aafa 100644 --- a/infer/src/biabduction/Prop.ml +++ b/infer/src/biabduction/Prop.ml @@ -111,21 +111,6 @@ let compare_prop p1 p2 = compare (fun _ _ -> 0) p1 p2 (** {1 Functions for Pretty Printing} *) -(** Pretty print a footprint. *) -let pp_footprint pe_ f fp = - let pe = {pe_ with Pp.cmap_norm= pe_.Pp.cmap_foot} in - let pp_pi f () = - if fp.pi_fp <> [] then - F.fprintf f "%a ;@\n" - (Pp.semicolon_seq ~print_env:{pe with break_lines= false} (Sil.pp_atom pe)) - fp.pi_fp - in - if fp.pi_fp <> [] || fp.sigma_fp <> [] then - F.fprintf f "@\n[footprint@\n @[%a%a@] ]" pp_pi () - (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred pe)) - fp.sigma_fp - - let pp_texp_simple pe = match pe.Pp.opt with SIM_DEFAULT -> Sil.pp_texp pe | SIM_WITH_TYP -> Sil.pp_texp_full pe @@ -294,9 +279,7 @@ let create_pvar_env (sigma : sigma) : Exp.t -> Exp.t = (** Update the object substitution given the stack variables in the prop *) -let prop_update_obj_sub pe prop = - if !Config.pp_simple then Pp.set_obj_sub pe (create_pvar_env prop.sigma) else pe - +let prop_update_obj_sub pe prop = Pp.set_obj_sub pe (create_pvar_env prop.sigma) (** Pretty print a footprint in simple mode. *) let pp_footprint_simple pe_ env f fp = @@ -326,21 +309,19 @@ let pp_prop pe0 f prop = if subl <> [] then F.fprintf f "%a ;@\n" (pp_subl pe) subl ; if pi <> [] then F.fprintf f "%a ;@\n" (pp_pi pe) pi in - if !Config.pp_simple then - let env = prop_pred_env prop in - let iter_f n hpara = F.fprintf f "@,@[%a@]" (pp_hpara_simple pe env n) hpara in - let iter_f_dll n hpara_dll = - F.fprintf f "@,@[%a@]" (pp_hpara_dll_simple pe env n) hpara_dll - in - let pp_predicates _ () = - if Sil.Predicates.is_empty env then () - else ( - F.fprintf f "@,where" ; - Sil.Predicates.iter env iter_f iter_f_dll ) - in - F.fprintf f "%a%a%a%a" pp_pure () (pp_sigma_simple pe env) prop.sigma - (pp_footprint_simple pe env) prop pp_predicates () - else F.fprintf f "%a%a%a" pp_pure () (pp_sigma pe) prop.sigma (pp_footprint pe) prop + let env = prop_pred_env prop in + let iter_f n hpara = F.fprintf f "@,@[%a@]" (pp_hpara_simple pe env n) hpara in + let iter_f_dll n hpara_dll = + F.fprintf f "@,@[%a@]" (pp_hpara_dll_simple pe env n) hpara_dll + in + let pp_predicates _ () = + if Sil.Predicates.is_empty env then () + else ( + F.fprintf f "@,where" ; + Sil.Predicates.iter env iter_f iter_f_dll ) + in + F.fprintf f "%a%a%a%a" pp_pure () (pp_sigma_simple pe env) prop.sigma + (pp_footprint_simple pe env) prop pp_predicates () in match pe0.Pp.kind with | Pp.HTML ->