From e2fb879321ea9d9ef7f8c82126a83b8589e60e9e Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Thu, 1 Oct 2015 07:18:59 -0700 Subject: [PATCH] make summaries deterministic by default by removing timing information Reviewed By: @martinoluca Differential Revision: D2475927 --- infer/src/backend/config.ml | 4 ++++ infer/src/backend/specs.ml | 15 ++++++++++----- 2 files changed, 14 insertions(+), 5 deletions(-) diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 6cbefb12f..998fc70b9 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -281,6 +281,10 @@ let type_size = ref false (** if true, compact summaries before saving *) let save_compact_summaries = ref true +(** If true, save the execution time in summaries. + This makes the analysis nondeterministic. *) +let save_time_in_summaries = ref false + (** flag: if true enables printing proposition compatible for the SMT project *) let smt_output = ref false diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 571323c7b..3f3ffc015 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -529,11 +529,16 @@ let store_summary pname (summ: summary) = let process_payload = function | PrePosts specs -> PrePosts (list_map NormSpec.erase_join_info_pre specs) | TypeState typestate_opt -> TypeState typestate_opt in - let summ' = { summ with payload = process_payload summ.payload } in - let summ'' = if !Config.save_compact_summaries - then summary_compact (Sil.create_sharing_env ()) summ' - else summ' in - Serialization.to_file summary_serializer (res_dir_specs_filename pname) summ'' + let summ1 = { summ with payload = process_payload summ.payload } in + 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 + Serialization.to_file summary_serializer (res_dir_specs_filename pname) summ3 (** Load procedure summary from the given file *) let load_summary specs_file =