diff --git a/infer/src/IR/BuiltinDecl.ml b/infer/src/IR/BuiltinDecl.ml index efa06211d..a83e5a512 100644 --- a/infer/src/IR/BuiltinDecl.ml +++ b/infer/src/IR/BuiltinDecl.ml @@ -68,8 +68,14 @@ let __infer_assume = create_procname "__infer_assume" let __infer_fail = create_procname "__infer_fail" +let __infer_generic_selection_expr = Procname.from_string_c_fun "__infer_generic_selection_expr" + let __infer_skip = create_procname "__infer_skip" +let __infer_skip_function = Procname.from_string_c_fun "__infer_skip_function" + +let __infer_skip_gcc_asm_stmt = Procname.from_string_c_fun "__infer_skip_gcc_asm_stmt" + let __instanceof = create_procname "__instanceof" let __method_set_ignore_attribute = create_procname "__method_set_ignore_attribute" diff --git a/infer/src/IR/BuiltinDecl.mli b/infer/src/IR/BuiltinDecl.mli index ab78793e0..83bcbce72 100644 --- a/infer/src/IR/BuiltinDecl.mli +++ b/infer/src/IR/BuiltinDecl.mli @@ -12,3 +12,9 @@ open! IStd include BUILTINS.S with type t = Procname.t val is_declared : Procname.t -> bool + +val __infer_skip_function : Procname.t + +val __infer_skip_gcc_asm_stmt : Procname.t + +val __infer_generic_selection_expr : Procname.t diff --git a/infer/src/clang/cFrontend_config.ml b/infer/src/clang/cFrontend_config.ml index a7f9db0a9..50ad7fb95 100644 --- a/infer/src/clang/cFrontend_config.ml +++ b/infer/src/clang/cFrontend_config.ml @@ -67,12 +67,6 @@ let id_cl = "id" let infer = "infer" -let infer_skip_fun = "__infer_skip_function" - -let infer_skip_gcc_asm_stmt = "__infer_skip_gcc_asm_stmt" - -let infer_generic_selection_expr = "__infer_generic_selection_expr" - let init = "init" let is_kind_of_class = "isKindOfClass:" diff --git a/infer/src/clang/cFrontend_config.mli b/infer/src/clang/cFrontend_config.mli index 6a2971996..b2ee3798f 100644 --- a/infer/src/clang/cFrontend_config.mli +++ b/infer/src/clang/cFrontend_config.mli @@ -59,12 +59,6 @@ val id_cl : string val infer : string -val infer_skip_fun : string - -val infer_skip_gcc_asm_stmt : string - -val infer_generic_selection_expr : string - val init : string val is_kind_of_class : string diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index a10033e74..48889e715 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -3094,15 +3094,13 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s and gccAsmStmt_trans trans_state stmt_info stmts = - let pname = Procname.from_string_c_fun CFrontend_config.infer_skip_gcc_asm_stmt in - call_function_with_args Procdesc.Node.GCCAsmStmt pname trans_state stmt_info (Typ.mk Tvoid) - stmts + call_function_with_args Procdesc.Node.GCCAsmStmt BuiltinDecl.__infer_skip_gcc_asm_stmt + trans_state stmt_info (Typ.mk Tvoid) stmts and genericSelectionExprUnknown_trans trans_state stmt_info stmts = - let pname = Procname.from_string_c_fun CFrontend_config.infer_generic_selection_expr in - call_function_with_args Procdesc.Node.GenericSelectionExpr pname trans_state stmt_info - (Typ.mk Tvoid) stmts + call_function_with_args Procdesc.Node.GenericSelectionExpr + BuiltinDecl.__infer_generic_selection_expr trans_state stmt_info (Typ.mk Tvoid) stmts and objc_cxx_throw_trans trans_state stmt_info stmts = @@ -3111,8 +3109,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s and cxxPseudoDestructorExpr_trans () = - let fun_name = Procname.from_string_c_fun CFrontend_config.infer_skip_fun in - mk_trans_result (Exp.Const (Const.Cfun fun_name), Typ.mk Tvoid) empty_control + mk_trans_result + (Exp.Const (Const.Cfun BuiltinDecl.__infer_skip_function), Typ.mk Tvoid) + empty_control and cxxTypeidExpr_trans trans_state stmt_info stmts expr_info = @@ -3171,12 +3170,11 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s stmt_info in let typ = CType_decl.qual_type_to_sil_type tenv expr_info.Clang_ast_t.ei_qual_type in - let fun_name = Procname.from_string_c_fun CFrontend_config.infer_skip_fun in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in let trans_state_param = {trans_state_pri with succ_nodes= []} in let res_trans_subexpr_list = List.map ~f:(instruction trans_state_param) stmts in let params = collect_returns res_trans_subexpr_list in - let sil_fun = Exp.Const (Const.Cfun fun_name) in + let sil_fun = Exp.Const (Const.Cfun BuiltinDecl.__infer_skip_function) in let ret_id = Ident.create_fresh Ident.knormal in let ret_exp = Exp.Var ret_id in let call_instr = Sil.Call ((ret_id, typ), sil_fun, params, sil_loc, CallFlags.default) in