diff --git a/infer/src/IR/BUILTINS.ml b/infer/src/IR/BUILTINS.ml index 598908dc5..08088b85a 100644 --- a/infer/src/IR/BUILTINS.ml +++ b/infer/src/IR/BUILTINS.ml @@ -38,7 +38,7 @@ module type S = sig val __exit : t - val __free_cf : t + val __objc_bridge_transfer : t val __get_array_length : t diff --git a/infer/src/IR/BuiltinDecl.ml b/infer/src/IR/BuiltinDecl.ml index 03c99a6d6..5e4411ab0 100644 --- a/infer/src/IR/BuiltinDecl.ml +++ b/infer/src/IR/BuiltinDecl.ml @@ -58,7 +58,7 @@ let __delete_locked_attribute = create_procname "__delete_locked_attribute" let __exit = create_procname "_exit" -let __free_cf = create_procname "__free_cf" +let __objc_bridge_transfer = create_procname "__objc_bridge_transfer" let __get_array_length = create_procname "__get_array_length" diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index b4a4cfd1f..7246ff0ad 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -516,13 +516,6 @@ let execute_free mk ?(mark_as_freed = true) raise (Exceptions.Wrong_argument_number __POS__) -(* This is for objects of CoreFoundation and CoreGraphics that ned to be released. - However, we want to treat them a bit differently to standard free; in particular we - don't want to flag Use_after_free because they can be used after CFRelease. The main purpose - of this builtin is to remove the memory attribute so that we don't report Memory Leaks. - This should behave correctly most of the time. *) -let execute_free_cf mk = execute_free mk ~mark_as_freed:false - let execute_alloc mk can_return_null {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; ret_id_typ; args; loc} : Builtin.ret_typ = @@ -863,7 +856,7 @@ let __delete_locked_attribute = let __exit = Builtin.register BuiltinDecl.__exit execute_exit -let __free_cf = Builtin.register BuiltinDecl.__free_cf (execute_free_cf PredSymb.Mmalloc) +let __objc_bridge_transfer = Builtin.register BuiltinDecl.__objc_bridge_transfer execute_skip (* return the length of the array passed as a parameter *) let __get_array_length = Builtin.register BuiltinDecl.__get_array_length execute___get_array_length diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 913506726..3507e7a16 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -388,8 +388,8 @@ let cpp_new_trans integer_type_widths sil_loc function_type size_exp placement_a mk_trans_result (exp, function_type) {empty_control with instrs= stmt_call} -let create_call_to_free_cf sil_loc exp typ = - let pname = BuiltinDecl.__free_cf in +let create_call_to_objc_bridge_transfer sil_loc exp typ = + let pname = BuiltinDecl.__objc_bridge_transfer in let stmt_call = Sil.Call ( (Ident.create_fresh Ident.knormal, Typ.void) @@ -456,7 +456,7 @@ let cast_operation ?objc_bridge_cast_kind cast_kind ((exp, typ) as exp_typ) cast | _ -> ( match objc_bridge_cast_kind with | Some `OBC_BridgeTransfer -> - let instr = create_call_to_free_cf sil_loc exp typ in + let instr = create_call_to_objc_bridge_transfer sil_loc exp typ in ([instr], (exp, cast_typ)) | Some cast_kind -> L.debug Capture Verbose diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 44f66030b..1384fc3c9 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -889,7 +889,7 @@ module ProcNameDispatcher = struct <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release ; -"CFAutorelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release ; -"CFBridgingRelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release - ; +match_builtin BuiltinDecl.__free_cf + ; +match_builtin BuiltinDecl.__objc_bridge_transfer <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release ; +match_builtin BuiltinDecl.__objc_alloc_no_fail <>$ capt_exp $--> ObjC.alloc_not_null ] ) end