[config] delete --precondition-stats option

Summary: Old option of yore, don't think anyone uses it anymore.

Reviewed By: ngorogiannis

Differential Revision: D20362652

fbshipit-source-id: c0a465cb4

infer/man/man1/infer-full.txt

@@ -1575,10 +1575,6 @@ INTERNAL OPTIONS
        --perf-profiler-data-file-reset
            Cancel the effect of --perf-profiler-data-file.
 
-       --precondition-stats
-           Activates: Print stats about preconditions to standard output
-           (Conversely: --no-precondition-stats)
-
        --print-buckets
            Activates: Show the internal bucket of Infer reports in their
            textual description (Conversely: --no-print-buckets)

infer/src/backend/InferPrint.ml

@@ -372,44 +372,6 @@ let pp_text_of_report fmt report =
   List.iter ~f:pp_row report ; F.fprintf fmt "@?"
 
 
-(** Categorize the preconditions of specs and print stats *)
-module PreconditionStats = struct
-  let nr_nopres = ref 0
-
-  let nr_empty = ref 0
-
-  let nr_onlyallocation = ref 0
-
-  let nr_dataconstraints = ref 0
-
-  let do_summary proc_name summary =
-    let specs = Tabulation.get_specs_from_payload summary in
-    let preconditions =
-      List.map ~f:(fun spec -> BiabductionSummary.Jprop.to_prop spec.BiabductionSummary.pre) specs
-    in
-    match Prop.CategorizePreconditions.categorize preconditions with
-    | Prop.CategorizePreconditions.Empty ->
-        incr nr_empty ;
-        L.result "Procedure: %a footprint:Empty@." Procname.pp proc_name
-    | Prop.CategorizePreconditions.OnlyAllocation ->
-        incr nr_onlyallocation ;
-        L.result "Procedure: %a footprint:OnlyAllocation@." Procname.pp proc_name
-    | Prop.CategorizePreconditions.NoPres ->
-        incr nr_nopres ;
-        L.result "Procedure: %a footprint:NoPres@." Procname.pp proc_name
-    | Prop.CategorizePreconditions.DataConstraints ->
-        incr nr_dataconstraints ;
-        L.result "Procedure: %a footprint:DataConstraints@." Procname.pp proc_name
-
-
-  let pp_stats () =
-    L.result "@.Precondition stats@." ;
-    L.result "Procedures with no preconditions: %d@." !nr_nopres ;
-    L.result "Procedures with empty precondition: %d@." !nr_empty ;
-    L.result "Procedures with only allocation conditions: %d@." !nr_onlyallocation ;
-    L.result "Procedures with data constraints: %d@." !nr_dataconstraints
-end
-
 module SummaryStats = struct
   module MetricTypes = struct
     type 't typ = Bool : bool typ | Int : int typ
@@ -724,7 +686,6 @@ let pp_lint_issues filters formats_by_report_kind linereader procname error_log
 let process_summary formats_by_report_kind summary issues_acc =
   let proc_name = Summary.get_proc_name summary in
   let issues_acc' = pp_summary_by_report_kind formats_by_report_kind summary issues_acc in
-  if Config.precondition_stats then PreconditionStats.do_summary proc_name summary ;
   if Config.summary_stats then SummaryStats.do_summary proc_name summary ;
   issues_acc'
 
@@ -797,7 +758,6 @@ let pp_summary_and_issues formats_by_report_kind issue_formats =
         ~f:(fun issue_format -> pp_issue_in_format issue_format error_filter issue)
         issue_formats )
     !all_issues ;
-  if Config.precondition_stats then PreconditionStats.pp_stats () ;
   if Config.summary_stats then SummaryStats.pp_stats () ;
   (* Issues that are generated and stored outside of summaries by linter and checkers *)
   List.iter (Config.lint_issues_dir_name :: FileLevelAnalysisIssueDirs.get_registered_dir_names ())

infer/src/base/Config.ml

@@ -1730,11 +1730,6 @@ and pmd_xml =
     "Output issues in (PMD) XML format"
 
 
-and precondition_stats =
-  CLOpt.mk_bool ~deprecated:["precondition_stats"] ~long:"precondition-stats"
-    "Print stats about preconditions to standard output"
-
-
 and print_active_checkers =
   CLOpt.mk_bool ~long:"print-active-checkers"
     ~in_help:InferCommand.[(Analyze, manual_generic)]
@@ -2894,8 +2889,6 @@ and patterns_skip_translation = match patterns_skip_translation with k, r -> (k,
 
 and pmd_xml = !pmd_xml
 
-and precondition_stats = !precondition_stats
-
 and print_active_checkers = !print_active_checkers
 
 and print_builtins = !print_builtins

infer/src/base/Config.mli

@@ -479,8 +479,6 @@ val perf_profiler_data_file : string option
 
 val pmd_xml : bool
 
-val precondition_stats : bool
-
 val print_active_checkers : bool
 
 val print_builtins : bool