Remove dead Config.pp_simple

Reviewed By: jeremydubreil

Differential Revision: D9751480

fbshipit-source-id: 1aa91b760

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 "")

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'
 
 

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 =

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

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

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 "@,@[<h>%a@]" (pp_hpara_simple pe env n) hpara in
-      let iter_f_dll n hpara_dll =
-        F.fprintf f "@,@[<h>%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 "@,@[<h>%a@]" (pp_hpara_simple pe env n) hpara in
+    let iter_f_dll n hpara_dll =
+      F.fprintf f "@,@[<h>%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 ->