diff --git a/infer/src/backend/InferAnalyze.re b/infer/src/backend/InferAnalyze.re index af51dc337..b200bd457 100644 --- a/infer/src/backend/InferAnalyze.re +++ b/infer/src/backend/InferAnalyze.re @@ -21,11 +21,19 @@ let analyze_exe_env_tasks cluster exe_env :Tasks.t => { L.log_progress_file (); Specs.clear_spec_tbl (); Random.self_init (); - 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 */ + 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 */ Tasks.create (Interproc.do_analysis_closures exe_env) continuation::( @@ -44,17 +52,6 @@ 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 bf8b3d0a5..b1a3a9efc 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -216,6 +216,7 @@ 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 @@ -247,7 +248,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 Config.biabduction && Ident.equal id id0 && not (Pvar.is_frontend_tmp pvar) -> + when is_infer && 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 5b25474cc..c5a3c9aac 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -615,6 +615,10 @@ 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" @@ -1609,11 +1613,11 @@ let post_parsing_initialization command_opt = linters_def_file := linters_def_default_file :: !linters_def_file; (match !analyzer with - | Some BiAbduction -> biabduction := true - | Some Crashcontext -> crashcontext := true - | Some Eradicate -> eradicate := true - | Some Tracing -> biabduction := true; tracing := true - | Some (CaptureOnly | CompileOnly | Checkers | Linters) -> () + | 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) -> () | None -> let open CLOpt in match command_opt with @@ -1697,6 +1701,7 @@ 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 48342e183..2df6c1a65 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -190,6 +190,7 @@ 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 829bd99aa..dd0872715 100644 --- a/infer/src/base/ZipLib.ml +++ b/infer/src/base/ZipLib.ml @@ -79,7 +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 not Config.biabduction then + if Config.checkers then zip_libs else if (Sys.file_exists Config.models_jar) = `Yes then (mk_zip_lib true Config.models_jar) :: zip_libs