[infer][ondemand] no need to pass the procedure name to save a summary

Summary: I accidentally save a summary with the wrong procedure name, which was affecting the analysis in some weird way. This makes this case no longer possible

Reviewed By: cristianoc

Differential Revision: D4654002

fbshipit-source-id: 9fcbe4e
master
Jeremy Dubreil 8 years ago committed by Facebook Github Bot
parent 6c14647eae
commit 13e199a4ca

@ -181,7 +181,7 @@ let iterate_callbacks call_graph exe_env =
(* Store all the summaries to disk *) (* Store all the summaries to disk *)
List.iter List.iter
~f:(fun pname -> ~f:(fun pname ->
Specs.store_summary pname (Specs.get_summary_unsafe "Checkers: store summaries" pname)) Specs.store_summary (Specs.get_summary_unsafe "Checkers: store summaries" pname))
procs_to_analyze; procs_to_analyze;
Config.curr_language := saved_language Config.curr_language := saved_language

@ -143,7 +143,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
let postprocess source summary = let postprocess source summary =
decr nesting; decr nesting;
Specs.store_summary callee_pname summary; Specs.store_summary summary;
Printer.write_proc_html source false callee_pdesc; Printer.write_proc_html source false callee_pdesc;
summary in summary in
@ -154,7 +154,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
let payload = let payload =
{ prev_summary.Specs.payload with Specs.preposts = Some []; } in { prev_summary.Specs.payload with Specs.preposts = Some []; } in
let new_summary = { prev_summary with Specs.stats; payload } in let new_summary = { prev_summary with Specs.stats; payload } in
Specs.store_summary callee_pname new_summary; Specs.store_summary new_summary;
new_summary in new_summary in
let old_state = save_global_state () in let old_state = save_global_state () in

@ -545,25 +545,10 @@ let summary_exists_in_models pname =
let summary_serializer : summary Serialization.serializer = let summary_serializer : summary Serialization.serializer =
Serialization.create_serializer Serialization.Key.summary Serialization.create_serializer Serialization.Key.summary
(** Save summary for the procedure into the spec database *)
let store_summary pname (summ1: summary) =
let summ2 = if Config.save_compact_summaries
then summary_compact (Sil.create_sharing_env ()) summ1
else summ1 in
let summ3 = if Config.save_time_in_summaries
then summ2
else
{ summ2 with
stats = { summ1.stats with stats_time = 0.0} } in
let final_summary = { summ3 with status = Analyzed } in
add_summary pname summ3 (* Make sure the summary in memory is identical to the saved one *);
Serialization.write_to_file summary_serializer (res_dir_specs_filename pname) ~data:final_summary
(** Load procedure summary from the given file *) (** Load procedure summary from the given file *)
let load_summary specs_file = let load_summary specs_file =
Serialization.read_from_file summary_serializer specs_file Serialization.read_from_file summary_serializer specs_file
(** Load procedure summary for the given procedure name and update spec table *) (** Load procedure summary for the given procedure name and update spec table *)
let load_summary_to_spec_table proc_name = let load_summary_to_spec_table proc_name =
let add summ = let add summ =
@ -702,6 +687,25 @@ let get_specs proc_name =
let get_phase summary = let get_phase summary =
summary.phase summary.phase
(** Save summary for the procedure into the spec database *)
let store_summary (summ1: summary) =
let summ2 = if Config.save_compact_summaries
then summary_compact (Sil.create_sharing_env ()) summ1
else summ1 in
let summ3 = if Config.save_time_in_summaries
then summ2
else
{ summ2 with
stats = { summ1.stats with stats_time = 0.0} } in
let final_summary = { summ3 with status = Analyzed } in
let proc_name = get_proc_name final_summary in
(* Make sure the summary in memory is identical to the saved one *)
add_summary proc_name final_summary;
Serialization.write_to_file
summary_serializer
(res_dir_specs_filename proc_name)
~data:final_summary
(** Set the current status for the proc *) (** Set the current status for the proc *)
let set_status proc_name status = let set_status proc_name status =
match get_summary proc_name with match get_summary proc_name with

@ -274,7 +274,7 @@ val spec_normalize : Tenv.t -> Prop.normal spec -> NormSpec.t
val res_dir_specs_filename : Procname.t -> DB.filename val res_dir_specs_filename : Procname.t -> DB.filename
(** Save summary for the procedure into the spec database *) (** Save summary for the procedure into the spec database *)
val store_summary : Procname.t -> summary -> unit val store_summary : summary -> unit
(** Return a compact representation of the summary *) (** Return a compact representation of the summary *)
val summary_compact : Sil.sharing_env -> summary -> summary val summary_compact : Sil.sharing_env -> summary -> summary

@ -39,7 +39,7 @@ module Make (H : Helper) = struct
match Specs.get_summary pname with match Specs.get_summary pname with
| Some global_summary -> | Some global_summary ->
let payload = H.update_payload summary global_summary.Specs.payload in let payload = H.update_payload summary global_summary.Specs.payload in
Specs.store_summary pname { global_summary with payload; } Specs.store_summary { global_summary with payload; }
| None -> | None ->
failwithf "Summary for %a should exist, but does not!@." Procname.pp pname failwithf "Summary for %a should exist, but does not!@." Procname.pp pname

Loading…
Cancel
Save