diff --git a/infer/src/backend/fork.ml b/infer/src/backend/fork.ml index ab113090d..046eceef2 100644 --- a/infer/src/backend/fork.ml +++ b/infer/src/backend/fork.ml @@ -97,9 +97,9 @@ module SpecMap = Map.Make (struct end) (** Update the specs of the current proc after the execution of one phase *) -let update_specs proc_name (new_specs : Specs.NormSpec.t list) : Specs.NormSpec.t list * bool = +let update_specs proc_name phase (new_specs : Specs.NormSpec.t list) + : Specs.NormSpec.t list * bool = let new_specs = Specs.normalized_specs_to_specs new_specs in - let phase = Specs.get_phase proc_name in let old_specs = Specs.get_specs proc_name in let changed = ref false in let current_specs = diff --git a/infer/src/backend/fork.mli b/infer/src/backend/fork.mli index 8d4e04ed9..d8753d2dc 100644 --- a/infer/src/backend/fork.mli +++ b/infer/src/backend/fork.mli @@ -34,7 +34,8 @@ val should_perform_transition : Cg.t -> Procname.t -> Procname.t list val transition_footprint_re_exe : Procname.t -> Prop.normal Specs.Jprop.t list -> unit (** Update the specs of the current proc after the execution of one phase *) -val update_specs : Procname.t -> Specs.NormSpec.t list -> Specs.NormSpec.t list * bool +val update_specs : + Procname.t -> Specs.phase -> Specs.NormSpec.t list -> Specs.NormSpec.t list * bool type analyze_proc = Exe_env.t -> Procname.t -> Specs.summary diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index bf688a0d0..14d51ef4a 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -128,13 +128,19 @@ let arg_desc = exit 1 end; source_path := s in + let incremental_changed_only () = + Config.ondemand_enabled := false; + incremental_mode := ANALYZE_CHANGED_ONLY in + let incremental () = + Config.ondemand_enabled := false; + incremental_mode := ANALYZE_CHANGED_AND_DEPENDENCIES in let desc = base_arg_desc @ [ "-err_file", Arg.Set_string err_file_cmdline, Some "file", "use file for the err channel"; "-exclude", Arg.String exclude, Some "file", "exclude from analysis the files and directories specified in file"; - "-incremental_changed_only", Arg.Unit (fun () -> incremental_mode := ANALYZE_CHANGED_ONLY), None, "only analyze files captured since the last analysis"; - "-incremental", Arg.Unit (fun () -> incremental_mode := ANALYZE_CHANGED_AND_DEPENDENCIES), None, "analyze files captured since the last analysis plus any dependencies"; + "-incremental_changed_only", Arg.Unit incremental_changed_only, None, "only analyze files captured since the last analysis"; + "-incremental", Arg.Unit incremental, None, "analyze files captured since the last analysis plus any dependencies"; "-iterations", Arg.Set_int iterations_cmdline, Some "n", "set the max number of operations for each function, expressed as a multiple of symbolic operations (default n=1)"; "-nonstop", Arg.Set Config.nonstop, None, "activate the nonstop mode: the analysis continues after finding errors. With this option the analysis can become less precise."; "-out_file", Arg.Set_string out_file_cmdline, Some "file", "use file for the out channel"; diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 710dedfda..48abf1f55 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -640,7 +640,7 @@ let report_context_leaks pname sigma tenv = (fun exps hpred -> match hpred with | Sil.Hpointsto (_, Sil.Eexp (exp, _), Sil.Sizeof (Sil.Tptr (typ, _), _)) when AndroidFramework.is_context typ tenv - && not (AndroidFramework.is_application typ tenv) -> + && not (AndroidFramework.is_application typ tenv) -> (exp, typ) :: exps | _ -> exps) [] @@ -894,7 +894,7 @@ let pp_intra_stats cfg proc_desc fmt proc_name = This function is architected so that [get_results ()] can be called even after [go ()] was interrupted by and exception. *) let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) - : (unit -> unit) * (unit -> Prop.normal Specs.spec list) = + : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) = let start_node = Cfg.Procdesc.get_start_node pdesc in let check_recursion_level () = @@ -906,7 +906,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t raise (Analysis_failure_exe (FKrecursion_timeout recursion_level)) end in - let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list) = + let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) = let go () = let init_prop = initial_prop_from_emp tenv pdesc in let init_props_from_pres = (* use existing pre's (in recursion some might exist) as starting points *) @@ -949,10 +949,11 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in Reporting.log_error pname ~pre: pre_opt exn; [] (* retuning no specs *) in - specs in + specs, Specs.FOOTPRINT in go, get_results in - let re_execution proc_name : (unit -> unit) * (unit -> Prop.normal Specs.spec list) = + let re_execution proc_name + : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) = let candidate_preconditions = IList.map (fun spec -> spec.Specs.pre) (Specs.get_specs proc_name) in let valid_specs = ref [] in let go () = @@ -991,7 +992,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t L.out "@. *** VALID PRECONDITIONS FOR %a: " Procname.pp proc_name; L.out "@.================================================@."; L.out "@.%a @.@." (Specs.Jprop.pp_list pe_text true) valid_preconditions; - specs in + specs, Specs.RE_EXECUTION in go, get_results in match Specs.get_phase pname with @@ -1109,25 +1110,28 @@ let report_custom_errors tenv cfg pdesc summary = (** update a summary after analysing a procedure *) -let update_summary prev_summary specs proc_name elapsed res = +let update_summary prev_summary specs phase proc_name elapsed res = let normal_specs = IList.map Specs.spec_normalize specs in - let new_specs, changed = Fork.update_specs proc_name normal_specs in + let new_specs, changed = Fork.update_specs proc_name phase normal_specs in let timestamp = max 1 (prev_summary.Specs.timestamp + if changed then 1 else 0) in let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in let symops = prev_summary.Specs.stats.Specs.symops + SymOp.get_total () in - let failure = match res with + let stats_failure = match res with | None -> prev_summary.Specs.stats.Specs.stats_failure | Some failure_kind -> res in let stats = { prev_summary.Specs.stats with - Specs.stats_time = stats_time; - Specs.symops = symops; - Specs.stats_failure = failure; } in + Specs.stats_time; + symops; + stats_failure; + } in let payload = { prev_summary.Specs.payload with - Specs.preposts = Some new_specs; } in + Specs.preposts = Some new_specs; + } in { prev_summary with - Specs.stats; + Specs.phase; + stats; payload; timestamp; } @@ -1147,11 +1151,11 @@ let analyze_proc exe_env (proc_name: Procname.t) : Specs.summary = reset_global_counters cfg proc_name proc_desc; let go, get_results = perform_analysis_phase cfg tenv proc_name proc_desc in let res = Fork.Timeout.exe_timeout (Specs.get_iterations proc_name) go () in - let specs = get_results () in + let specs, phase = get_results () in let elapsed = Unix.gettimeofday () -. init_time in let prev_summary = Specs.get_summary_unsafe "analyze_proc" proc_name in let updated_summary = - update_summary prev_summary specs proc_name elapsed res in + update_summary prev_summary specs phase proc_name elapsed res in if !Config.curr_language == Config.C_CPP && Config.report_custom_error then report_custom_errors tenv cfg proc_desc updated_summary; if !Config.curr_language == Config.Java && !Config.report_runtime_exceptions then