diff --git a/infer/src/backend/InferAnalyze.re b/infer/src/backend/InferAnalyze.re index ac228a7ef..f02fcb01b 100644 --- a/infer/src/backend/InferAnalyze.re +++ b/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 + } + } + ] } }; diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index b1a3a9efc..bf8b3d0a5 100644 --- a/infer/src/backend/errdesc.ml +++ b/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: diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index c5a3c9aac..72b7d2de7 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 2df6c1a65..48342e183 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/base/ZipLib.ml b/infer/src/base/ZipLib.ml index dd0872715..6639e5141 100644 --- a/infer/src/base/ZipLib.ml +++ b/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