Skip cpp models from traces

Reviewed By: akotulski

Differential Revision: D3305691

fbshipit-source-id: 266b824

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
+  };

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;

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

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

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

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

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

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