diff --git a/infer/src/IR/AttributesTable.re b/infer/src/IR/AttributesTable.re index ce78f00e7..290aa9648 100644 --- a/infer/src/IR/AttributesTable.re +++ b/infer/src/IR/AttributesTable.re @@ -84,3 +84,13 @@ let get_correct_type_from_objc_class_name c => { Option.map (fun st => Sil.Tstruct st) (Tenv.lookup tenv type_name) } }; + + +/** Returns true if the method is defined as a C++ model */ +let pname_is_cpp_model callee_pname => + switch (load_attributes callee_pname) { + | Some attrs => + let file = DB.source_file_to_string attrs.ProcAttributes.loc.Location.file; + DB.file_is_in_cpp_model file + | None => false + }; diff --git a/infer/src/IR/AttributesTable.rei b/infer/src/IR/AttributesTable.rei index 177defe00..fe4c5aae3 100644 --- a/infer/src/IR/AttributesTable.rei +++ b/infer/src/IR/AttributesTable.rei @@ -28,3 +28,6 @@ let find_tenv_from_class_of_proc: Procname.t => option Tenv.t; /** defined. We do this by adding a method that is unique to each class, and then */ /** finding the tenv that corresponds to the class definition. */ let get_correct_type_from_objc_class_name: Mangled.t => option Sil.typ; + +/** Returns true if the method is defined as a C++ model */ +let pname_is_cpp_model : Procname.t => bool; diff --git a/infer/src/backend/DB.ml b/infer/src/backend/DB.ml index 9da1f910f..95dc14f4e 100644 --- a/infer/src/backend/DB.ml +++ b/infer/src/backend/DB.ml @@ -365,3 +365,9 @@ let file_was_updated_after_start fname = else (* since file doesn't exist, it wasn't modified *) false + +(** Returns true if the file is a C++ model *) +let file_is_in_cpp_model file = + let normalized_file_dir = filename_to_absolute (Filename.dirname file) in + let normalized_cpp_models_dir = filename_to_absolute Config.cpp_models_dir in + string_is_prefix normalized_cpp_models_dir normalized_file_dir diff --git a/infer/src/backend/DB.mli b/infer/src/backend/DB.mli index 2a01a468d..b4ccb8334 100644 --- a/infer/src/backend/DB.mli +++ b/infer/src/backend/DB.mli @@ -169,3 +169,6 @@ val global_tenv_fname : unit -> filename (** Check if a path is a Java, C, C++ or Objectve C source file according to the file extention *) val is_source_file: string -> bool + +(** Returns true if the file is a C++ model *) +val file_is_in_cpp_model : string -> bool diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 49e471115..18db9fc66 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -186,6 +186,13 @@ let models_dir = let lib_specs_dir = Filename.concat lib_dir specs_dir_name in lib_specs_dir +let cpp_models_dir = + let bin_dir = Filename.dirname Sys.executable_name in + let cpp_models_dir = + Filename.concat (Filename.concat bin_dir Filename.parent_dir_name) + "models/cpp/include" in + cpp_models_dir + let os_type = match Sys.os_type with | "Win32" -> Win32 | "Cygwin" -> Cygwin diff --git a/infer/src/backend/config.mli b/infer/src/backend/config.mli index d3be6598a..a9c9127bd 100644 --- a/infer/src/backend/config.mli +++ b/infer/src/backend/config.mli @@ -60,6 +60,7 @@ val log_analysis_crash : string val max_recursion : int val meet_level : int val models_dir : string +val cpp_models_dir : string val nsnotification_center_checker_backend : bool val objc_method_call_semantics : bool val os_type : os_type diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 7ff9d63ea..a2e1df643 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -664,7 +664,8 @@ let prop_set_exn pname prop se_exn = (** Include a subtrace for a procedure call if the callee is not a model. *) let include_subtrace callee_pname = - Specs.get_origin callee_pname <> DB.Models + Specs.get_origin callee_pname <> DB.Models && + not (AttributesTable.pname_is_cpp_model callee_pname) (** combine the spec's post with a splitting and actual precondition *) let combine diff --git a/infer/src/clang/cLocation.ml b/infer/src/clang/cLocation.ml index 41ff2d3b6..b408eb19d 100644 --- a/infer/src/clang/cLocation.ml +++ b/infer/src/clang/cLocation.ml @@ -118,9 +118,8 @@ let should_translate (loc_start, loc_end) decl_trans_context = in let file_in_project = map_path_of file_in_project loc_end || map_path_of file_in_project loc_start in - let file_in_models file = Str.string_match (Str.regexp "^.*/infer/models/cpp/include/") file 0 in - let file_in_models = map_path_of file_in_models loc_end - || map_path_of file_in_models loc_start in + let file_in_models = map_path_of DB.file_is_in_cpp_model loc_end + || map_path_of DB.file_is_in_cpp_model loc_start in equal_current_source !curr_file || map_file_of equal_current_source loc_end || map_file_of equal_current_source loc_start