diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index 4b06dd720..2b48b0703 100644 --- a/infer/src/backend/InferPrint.ml +++ b/infer/src/backend/InferPrint.ml @@ -521,15 +521,17 @@ module Stats = struct let num_preposts = match summary.payload.preposts with Some preposts -> List.length preposts | None -> 0 in + let lang = Specs.get_proc_name summary |> Typ.Procname.get_language in stats.events_to_log <- EventLogger.AnalysisStats { analysis_nodes_visited= IntSet.cardinal summary.stats.nodes_visited_re ; analysis_status= summary.stats.stats_failure ; analysis_total_nodes= Specs.get_proc_desc summary |> Procdesc.get_nodes_num - ; clang_method_kind= (Specs.get_attributes summary).clang_method_kind - ; lang= - Specs.get_proc_name summary |> Typ.Procname.get_language - |> Language.to_explicit_string + ; clang_method_kind= + ( if Language.equal lang Language.Clang then + Some (Specs.get_attributes summary).clang_method_kind + else None ) + ; lang= Language.to_explicit_string lang ; method_location= Specs.get_loc summary ; method_name= Specs.get_proc_name summary |> Typ.Procname.to_string ; num_preposts diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 42383af2d..43e384c94 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1307,9 +1307,8 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path prop path resolved_pname ret_annots loc ret_id ret_typ_opt n_actual_params ) | None -> - skip_call ~is_objc_instance_method:false - ~reason:"function or method not found" prop path resolved_pname ret_annots - loc ret_id ret_typ_opt n_actual_params + skip_call ~reason:"function or method not found" prop path resolved_pname + ret_annots loc ret_id ret_typ_opt n_actual_params else proc_call (Option.value_exn resolved_summary_opt) @@ -1716,6 +1715,7 @@ and sym_exec_alloc_model pname ret_typ tenv ret_id pdesc loc prop path : Builtin and proc_call callee_summary {Builtin.pdesc; tenv; prop_= pre; path; ret_id; args= actual_pars; loc} = let caller_pname = Procdesc.get_proc_name pdesc in + let callee_attrs = Specs.get_attributes callee_summary in let callee_pname = Specs.get_proc_name callee_summary in check_inherently_dangerous_function caller_pname callee_pname ; let formal_types = List.map ~f:snd (Specs.get_formals callee_summary) in @@ -1753,21 +1753,17 @@ and proc_call callee_summary to their actual type otherwise. The latter case happens with variable - arguments functions *) let actual_params = comb actual_pars formal_types in - (* In case we call an objc instance method we add and extra spec *) - (* were the receiver is null and the semantics of the call is nop*) - (* let callee_attrs = Specs.get_attributes callee_summary in *) - if !Language.curr_language <> Language.Java - && ProcAttributes.clang_method_kind_equal - (Specs.get_attributes callee_summary).ProcAttributes.clang_method_kind - ProcAttributes.OBJC_INSTANCE - then - handle_objc_instance_method_call actual_pars actual_params pre tenv ret_id pdesc callee_pname - loc path - (Tabulation.exe_function_call callee_summary) - else - (* non-objective-c method call. Standard tabulation *) - Tabulation.exe_function_call callee_summary tenv ret_id pdesc callee_pname loc actual_params - pre path + (* In case we call an objc instance method we add an extra spec + where the receiver is null and the semantics of the call is nop *) + match (!Language.curr_language, callee_attrs.ProcAttributes.clang_method_kind) with + | Language.Clang, ProcAttributes.OBJC_INSTANCE -> + handle_objc_instance_method_call actual_pars actual_params pre tenv ret_id pdesc callee_pname + loc path + (Tabulation.exe_function_call callee_summary) + | _ -> + (* non-objective-c method call. Standard tabulation *) + Tabulation.exe_function_call callee_summary tenv ret_id pdesc callee_pname loc actual_params + pre path (** perform symbolic execution for a single prop, and check for junk *) diff --git a/infer/src/base/EventLogger.ml b/infer/src/base/EventLogger.ml index 9a9637533..23fe8ac43 100644 --- a/infer/src/base/EventLogger.ml +++ b/infer/src/base/EventLogger.ml @@ -75,7 +75,7 @@ type analysis_stats = { analysis_nodes_visited: int ; analysis_status: SymOp.failure_kind option ; analysis_total_nodes: int - ; clang_method_kind: ProcAttributes.clang_method_kind + ; clang_method_kind: ProcAttributes.clang_method_kind option ; lang: string ; method_location: Location.t ; method_name: string @@ -90,8 +90,8 @@ let create_analysis_stats_row base record = (Option.value_map record.analysis_status ~default:"OK" ~f:(fun stats_failure -> SymOp.failure_kind_to_string stats_failure )) |> add_int ~key:"analysis_total_nodes" ~data:record.analysis_total_nodes - |> add_string ~key:"clang_method_kind" - ~data:(ProcAttributes.string_of_clang_method_kind record.clang_method_kind) + |> add_string_opt ~key:"clang_method_kind" + ~data:(Option.map record.clang_method_kind ~f:ProcAttributes.string_of_clang_method_kind) |> add_string ~key:"lang" ~data:record.lang |> add_string ~key:"method_location" ~data: diff --git a/infer/src/base/EventLogger.mli b/infer/src/base/EventLogger.mli index 4aa3ffa75..26c605a34 100644 --- a/infer/src/base/EventLogger.mli +++ b/infer/src/base/EventLogger.mli @@ -11,7 +11,7 @@ type analysis_stats = { analysis_nodes_visited: int ; analysis_status: SymOp.failure_kind option ; analysis_total_nodes: int - ; clang_method_kind: ProcAttributes.clang_method_kind + ; clang_method_kind: ProcAttributes.clang_method_kind option ; lang: string ; method_location: Location.t ; method_name: string