[infer][checkers] finaly remove the unecessary 'checkers' flag

Summary: This flag is no longer useful

Reviewed By: sblackshear

Differential Revision: D5081521

fbshipit-source-id: c6e9ba7

infer/src/backend/InferAnalyze.re

@@ -21,19 +21,11 @@ let analyze_exe_env_tasks cluster exe_env :Tasks.t => {
   L.log_progress_file ();
   Specs.clear_spec_tbl ();
   Random.self_init ();
-  if Config.checkers {
-    /* run the checkers only */
-    Tasks.create [
-      fun () => {
-        let call_graph = Exe_env.get_cg exe_env;
-        Callbacks.iterate_callbacks call_graph exe_env;
-        if Config.write_html {
-          Printer.write_all_html_files cluster
-        }
-      }
-    ]
-  } else {
-    /* run the full analysis */
+  let biabduction_only =
+    Config.equal_analyzer Config.analyzer Config.BiAbduction ||
+    Config.equal_analyzer Config.analyzer Config.Tracing;
+  if biabduction_only {
+    /* run the biabduction analysis only */
     Tasks.create
       (Interproc.do_analysis_closures exe_env)
       continuation::(
@@ -52,6 +44,17 @@ let analyze_exe_env_tasks cluster exe_env :Tasks.t => {
           None
         }
       )
+  } else {
+    /* run the registered checkers */
+    Tasks.create [
+      fun () => {
+        let call_graph = Exe_env.get_cg exe_env;
+        Callbacks.iterate_callbacks call_graph exe_env;
+        if Config.write_html {
+          Printer.write_all_html_files cluster
+        }
+      }
+    ]
   }
 };
 

infer/src/backend/errdesc.ml

@@ -216,7 +216,6 @@ let rec find_boolean_assignment node pvar true_branch : Procdesc.Node.t option =
 (** Find the Load instruction used to declare normal variable [id],
     and return the expression dereferenced to initialize [id] *)
 let rec _find_normal_variable_load tenv (seen : Exp.Set.t) node id : DExp.t option =
-  let is_infer = not (Config.checkers || Config.eradicate) in
   let find_declaration node = function
     | Sil.Load (id0, e, _, _) when Ident.equal id id0 ->
         if verbose
@@ -248,7 +247,7 @@ let rec _find_normal_variable_load tenv (seen : Exp.Set.t) node id : DExp.t opti
             List.map ~f:unNone args_dexpo in
         Some (DExp.Dretcall (fun_dexp, args_dexp, loc, call_flags))
     | Sil.Store (Exp.Lvar pvar, _, Exp.Var id0, _)
-      when is_infer && Ident.equal id id0 && not (Pvar.is_frontend_tmp pvar) ->
+      when Config.biabduction && Ident.equal id id0 && not (Pvar.is_frontend_tmp pvar) ->
         (* this case is a hack to make bucketing continue to work in the presence of copy
            propagation. previously, we would have code like:
            n1 = foo(); x = n1; n2 = x; n2.toString(), but copy-propagation will optimize this to:

infer/src/base/Config.ml

@@ -615,10 +615,6 @@ and checkers_repeated_calls =
   CLOpt.mk_bool ~long:"checkers-repeated-calls" ~in_help:CLOpt.[Analyze, manual_generic]
     "check for repeated calls"
 
-and checkers =
-  CLOpt.mk_bool ~long:"checkers" ~in_help:CLOpt.[Analyze, manual_generic]
-    "the checkers instead of the full analysis"
-
 and clang_biniou_file =
   CLOpt.mk_path_opt ~long:"clang-biniou-file"
     ~in_help:CLOpt.[Capture, manual_clang] ~meta:"file"
@@ -1613,17 +1609,17 @@ let post_parsing_initialization command_opt =
     linters_def_file := linters_def_default_file :: !linters_def_file;
 
   (match !analyzer with
-   | Some Checkers -> checkers := true
-   | Some Crashcontext -> checkers := true; crashcontext := true
-   | Some Eradicate -> checkers := true; eradicate := true
-   | Some Tracing -> tracing := true
-   | Some (CaptureOnly | CompileOnly | BiAbduction | Linters) -> ()
+   | Some BiAbduction -> biabduction := true
+   | Some Crashcontext -> crashcontext := true
+   | Some Eradicate -> eradicate := true
+   | Some Tracing -> biabduction := true; tracing := true
+   | Some (CaptureOnly | CompileOnly | Checkers | Linters) -> ()
    | None ->
        let open CLOpt in
        match command_opt with
        | Some Compile -> analyzer := Some CompileOnly
        | Some Capture -> analyzer := Some CaptureOnly
-       | _ -> ()
+       | _ -> biabduction := true (* the default option is to run the biabduction analysis *)
   );
   Option.value ~default:CLOpt.Run command_opt
 
@@ -1701,7 +1697,6 @@ and bugs_txt = !bugs_txt
 and changed_files_index = !changed_files_index
 and calls_csv = !calls_csv
 and dump_duplicate_symbols = !dump_duplicate_symbols
-and checkers = !checkers
 and checkers_repeated_calls = !checkers_repeated_calls
 and clang_biniou_file = !clang_biniou_file
 and clang_ignore_regex = !clang_ignore_regex

infer/src/base/Config.mli

@@ -190,7 +190,6 @@ val calls_csv : string option
 (** directory where the results of the capture phase are stored *)
 val captured_dir : string
 
-val checkers : bool
 val checkers_repeated_calls : bool
 val clang_biniou_file : string option
 val clang_frontend_action_string : string

infer/src/base/ZipLib.ml

@@ -79,9 +79,7 @@ let zip_libraries =
             (* fname is a dir of specs *)
             zip_libs in
         List.fold ~f:add_zip ~init:[] Config.specs_library in
-    if Config.checkers then
-      zip_libs
-    else if (Sys.file_exists Config.models_jar) = `Yes then
+    if Config.biabduction && (Sys.file_exists Config.models_jar) = `Yes then
       (mk_zip_lib true Config.models_jar) :: zip_libs
     else
       zip_libs