diff --git a/infer/src/IR/BUILTINS.mli b/infer/src/IR/BUILTINS.mli
new file mode 100644
index 000000000..3a56fcc22
--- /dev/null
+++ b/infer/src/IR/BUILTINS.mli
@@ -0,0 +1,85 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+(** List of all builtins that are interpreted specially by the backend *)
+module type S = sig
+  type t
+  val __assert_fail : t
+  val __builtin_va_arg : t
+  val __builtin_va_copy : t
+  val __builtin_va_end : t
+  val __builtin_va_start : t
+  val __cast : t (** [__cast(val,typ)] implements java's [typ(val)] *)
+
+  val __check_untainted : t
+  val __cxx_typeid : t
+  val __delete : t
+  val __delete_array : t
+  val __delete_locked_attribute : t
+  val __exit : t
+  val __get_array_length : t
+  val __get_hidden_field : t
+  val __get_type_of : t
+  val __infer_assume : t
+  val __infer_fail : t
+  val __instanceof : t (** [__instanceof(val,typ)] implements java's [val instanceof typ] *)
+
+  val __method_set_ignore_attribute : t
+  val __new : t
+  val __new_array : t
+  val __objc_alloc : t
+  val __objc_alloc_no_fail : t
+  val __objc_cast : t
+  val __objc_dictionary_literal : t
+  val __objc_release : t
+  val __objc_release_autorelease_pool : t
+  val __objc_release_cf : t
+  val __objc_retain : t
+  val __objc_retain_cf : t
+  val __placement_delete : t
+  val __placement_new : t
+  val __print_value : t
+  val __require_allocated_array : t
+  val __set_array_length : t
+  val __set_autorelease_attribute : t
+  val __set_file_attribute : t
+  val __set_hidden_field : t
+  val __set_lock_attribute : t
+  val __set_locked_attribute : t
+  val __set_mem_attribute : t
+  val __set_observer_attribute : t
+  val __set_taint_attribute : t
+  val __set_unlocked_attribute : t
+  val __set_unsubscribed_observer_attribute : t
+  val __set_untaint_attribute : t
+  val __split_get_nth : t
+  val __throw : t
+  val __unwrap_exception : t
+  val abort : t
+  val exit : t
+  val free : t
+  val fscanf : t
+  val fwscanf : t
+  val malloc : t
+  val malloc_no_fail : t
+  val nsArray_arrayWithObjects : t
+  val nsArray_arrayWithObjectsCount : t
+  val objc_cpp_throw : t
+  val pthread_create : t
+  val scanf : t
+  val sscanf : t
+  val swscanf : t
+  val vfscanf : t
+  val vfwscanf : t
+  val vscanf : t
+  val vsscanf : t
+  val vswscanf : t
+  val vwscanf : t
+  val wscanf : t
+end
diff --git a/infer/src/IR/BuiltinDecl.ml b/infer/src/IR/BuiltinDecl.ml
new file mode 100644
index 000000000..0eb458d04
--- /dev/null
+++ b/infer/src/IR/BuiltinDecl.ml
@@ -0,0 +1,100 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+type t = Procname.t
+
+let builtin_decls = ref Procname.Set.empty
+
+let register pname =
+  builtin_decls := Procname.Set.add pname !builtin_decls
+
+let create_procname name =
+  let pname = Procname.from_string_c_fun name in
+  register pname;
+  pname
+
+let create_objc_class_method class_name method_name =
+  let method_kind = Procname.ObjCClassMethod in
+  let pname = (Procname.ObjC_Cpp (Procname.objc_cpp class_name method_name method_kind)) in
+  register pname;
+  pname
+
+let is_declared pname = Procname.Set.mem pname !builtin_decls
+
+let __assert_fail = create_procname "__assert_fail"
+let __builtin_va_arg = create_procname "__builtin_va_arg"
+let __builtin_va_copy = create_procname "__builtin_va_copy"
+let __builtin_va_end = create_procname "__builtin_va_end"
+let __builtin_va_start = create_procname "__builtin_va_start"
+let __cast = create_procname "__cast"
+let __check_untainted = create_procname "__check_untainted"
+let __cxx_typeid = create_procname "__cxx_typeid"
+let __delete = create_procname "__delete"
+let __delete_array = create_procname "__delete_array"
+let __delete_locked_attribute = create_procname "__delete_locked_attribute"
+let __exit = create_procname "_exit"
+let __get_array_length = create_procname "__get_array_length"
+let __get_hidden_field = create_procname "__get_hidden_field"
+let __get_type_of = create_procname "__get_type_of"
+let __infer_assume = create_procname "__infer_assume"
+let __infer_fail = create_procname "__infer_fail"
+let __instanceof = create_procname "__instanceof"
+let __method_set_ignore_attribute = create_procname "__method_set_ignore_attribute"
+let __new = create_procname "__new"
+let __new_array = create_procname "__new_array"
+let __objc_alloc = create_procname "__objc_alloc"
+let __objc_alloc_no_fail = create_procname "__objc_alloc_no_fail"
+let __objc_cast = create_procname "__objc_cast"
+let __objc_dictionary_literal =
+  create_objc_class_method "NSDictionary" "dictionaryWithObjects:forKeys:count:"
+let __objc_release = create_procname "__objc_release"
+let __objc_release_autorelease_pool = create_procname "__objc_release_autorelease_pool"
+let __objc_release_cf = create_procname "__objc_release_cf"
+let __objc_retain = create_procname "__objc_retain"
+let __objc_retain_cf = create_procname "__objc_retain_cf"
+let __placement_delete = create_procname "__placement_delete"
+let __placement_new = create_procname "__placement_new"
+let __print_value = create_procname "__print_value"
+let __require_allocated_array = create_procname "__require_allocated_array"
+let __set_array_length = create_procname "__set_array_length"
+let __set_autorelease_attribute = create_procname "__set_autorelease_attribute"
+let __set_file_attribute = create_procname "__set_file_attribute"
+let __set_hidden_field = create_procname "__set_hidden_field"
+let __set_lock_attribute = create_procname "__set_lock_attribute"
+let __set_locked_attribute = create_procname "__set_locked_attribute"
+let __set_mem_attribute = create_procname "__set_mem_attribute"
+let __set_observer_attribute = create_procname "__set_observer_attribute"
+let __set_taint_attribute = create_procname "__set_taint_attribute"
+let __set_unlocked_attribute = create_procname "__set_unlocked_attribute"
+let __set_unsubscribed_observer_attribute = create_procname "__set_unsubscribed_observer_attribute"
+let __set_untaint_attribute = create_procname "__set_untaint_attribute"
+let __split_get_nth = create_procname "__split_get_nth"
+let __throw = create_procname "__throw"
+let __unwrap_exception = create_procname "__unwrap_exception"
+let abort = create_procname "abort"
+let exit = create_procname "exit"
+let free = create_procname "free"
+let fscanf = create_procname "fscanf"
+let fwscanf = create_procname "fwscanf"
+let malloc = create_procname "malloc"
+let malloc_no_fail = create_procname "malloc_no_fail"
+let nsArray_arrayWithObjects = create_objc_class_method "NSArray" "arrayWithObjects:"
+let nsArray_arrayWithObjectsCount = create_objc_class_method "NSArray" "arrayWithObjects:count:"
+let objc_cpp_throw = create_procname "__infer_objc_cpp_throw"
+let pthread_create = create_procname "pthread_create"
+let scanf = create_procname "scanf"
+let sscanf = create_procname "sscanf"
+let swscanf = create_procname "swscanf"
+let vfscanf = create_procname "vfscanf"
+let vfwscanf = create_procname "vfwscanf"
+let vscanf = create_procname "vscanf"
+let vsscanf = create_procname "vsscanf"
+let vswscanf = create_procname "vswscanf"
+let vwscanf = create_procname "vwscanf"
+let wscanf = create_procname "wscanf"
diff --git a/infer/src/IR/BuiltinDecl.mli b/infer/src/IR/BuiltinDecl.mli
new file mode 100644
index 000000000..a2adf83ff
--- /dev/null
+++ b/infer/src/IR/BuiltinDecl.mli
@@ -0,0 +1,15 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! Utils
+
+(** Procnames for the builtin functions supported *)
+include BUILTINS.S with type t = Procname.t
+
+val is_declared : Procname.t -> bool
diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/BuiltinDefn.ml
similarity index 82%
rename from infer/src/backend/modelBuiltins.ml
rename to infer/src/backend/BuiltinDefn.ml
index b16a296b1..7c888cf70 100644
--- a/infer/src/backend/modelBuiltins.ml
+++ b/infer/src/backend/BuiltinDefn.ml
@@ -16,6 +16,8 @@ open SymExec
 module L = Logging
 module F = Format
 
+type t = Builtin.registered
+
 let execute___no_op prop path: Builtin.ret_typ =
   [(prop, path)]
 
@@ -941,207 +943,10 @@ let execute___assert_fail { Builtin.pdesc; tenv; prop_; path; args; loc; }
     Sil.Store (Exp.Lvar Sil.custom_error, Typ.Tvoid, Exp.Const (Const.Cstr error_str), loc) in
   SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)]
 
-let __assert_fail = Builtin.register
-    "__assert_fail" execute___assert_fail
-let _ = Builtin.register
-    (* model for va_arg *)
-    "__builtin_va_arg" execute___builtin_va_arg
-let _ = Builtin.register
-    "__builtin_va_copy" execute_skip
-let _ = Builtin.register
-    (* model va_end as skip *)
-    "__builtin_va_end" execute_skip
-let _ = Builtin.register
-    "__builtin_va_start" execute_skip
-let __cast = Builtin.register
-    (* [__cast(val,typ)] implements java's [typ(val)] *)
-    "__cast" execute___cast
-let _ = Builtin.register
-    (* report a taint error if the parameter is tainted, and assume it is untainted afterward *)
-    "__check_untainted" execute___check_untainted
-let __delete = Builtin.register
-    (* like free *)
-    "__delete" (execute_free PredSymb.Mnew)
-let __delete_array = Builtin.register
-    (* like free *)
-    "__delete_array" (execute_free PredSymb.Mnew_array)
-let __exit = Builtin.register
-    (* _exit from C library *)
-    "_exit" execute_exit
-let __get_array_length = Builtin.register
-    (* return the length of the array passed as a parameter *)
-    "__get_array_length" execute___get_array_length
-let __require_allocated_array = Builtin.register
-    (* require the parameter to point to an allocated array *)
-    "__require_allocated_array" execute___require_allocated_array
-let _ = Builtin.register
-    (* return the value of a hidden field in the struct *)
-    "__get_hidden_field" execute___get_hidden_field
-let __get_type_of = Builtin.register
-    (* return the get the type of the allocated object passed as a parameter *)
-    "__get_type_of" execute___get_type_of
-let __infer_assume = Builtin.register
-    (* infer assume, diverging on inconsistencies *)
-    "__infer_assume" execute___infer_assume
-let __infer_fail = Builtin.register
-    (* externally create new errors *)
-    "__infer_fail" execute___infer_fail
-let __instanceof = Builtin.register
-    (* [__instanceof(val,typ)] implements java's [val instanceof typ] *)
-    "__instanceof" execute___instanceof
-let _ = Builtin.register
-    "__method_set_ignore_attribute" execute___method_set_ignore_attribute
-let __new = Builtin.register
-    (* like malloc, but always succeeds *)
-    "__new" (execute_alloc PredSymb.Mnew false)
-let __new_array = Builtin.register
-    (* like malloc, but always succeeds *)
-    "__new_array" (execute_alloc PredSymb.Mnew_array false)
-let __objc_alloc = Builtin.register
-    (* Objective C alloc *)
-    "__objc_alloc" (execute_alloc PredSymb.Mobjc true)
-let __objc_alloc_no_fail = Builtin.register
-    (* like __objc_alloc, but does not return nil *)
-    "__objc_alloc_no_fail" (execute_alloc PredSymb.Mobjc false)
-let __objc_cast = Builtin.register
-    (* objective-c "cast" *)
-    "__objc_cast" execute___objc_cast
-let __objc_release = Builtin.register
-    (* objective-c "release" *)
-    "__objc_release" execute___objc_release
-let __objc_release_autorelease_pool = Builtin.register
-    (* set the attribute of the parameter as autorelease *)
-    "__objc_release_autorelease_pool" execute___release_autorelease_pool
-let __objc_release_cf = Builtin.register
-    (* objective-c "release" *)
-    "__objc_release_cf" execute___objc_release_cf
-let __objc_retain = Builtin.register
-    (* objective-c "retain" *)
-    "__objc_retain" execute___objc_retain
-let __objc_retain_cf = Builtin.register
-    "__objc_retain_cf" execute___objc_retain_cf
-let __cxx_typeid = Builtin.register
-    (* C++ "typeid" *)
-    "__cxx_typeid" execute___cxx_typeid
-let __placement_delete = Builtin.register
-    (* placement delete is skip *)
-    "__placement_delete" execute_skip
-let __placement_new = Builtin.register
-    (* placement new returns the first argument *)
-    "__placement_new" execute_return_first_argument
-let _ = Builtin.register
-    (* print a value as seen by the engine *)
-    "__print_value" execute___print_value
-let __set_array_length = Builtin.register
-    (* set the length of the array passed as a parameter *)
-    "__set_array_length" execute___set_array_length
-let __set_autorelease_attribute = Builtin.register
-    (* set the attribute of the parameter as autorelease *)
-    "__set_autorelease_attribute" execute___set_autorelease_attribute
-let __set_file_attribute = Builtin.register
-    (* set the attribute of the parameter as file *)
-    "__set_file_attribute" execute___set_file_attribute
-let __set_lock_attribute = Builtin.register
-    (* set the attribute of the parameter as file *)
-    "__set_lock_attribute" execute___set_lock_attribute
-let __set_mem_attribute = Builtin.register
-    (* set the attribute of the parameter as memory *)
-    "__set_mem_attribute" execute___set_mem_attribute
-let __set_observer_attribute = Builtin.register
-    (* set the observer attribute of the parameter *)
-    "__set_observer_attribute" (execute___set_attr PredSymb.Aobserver)
-let __set_unsubscribed_observer_attribute = Builtin.register
-    (* set the unregistered observer attribute of the parameter *)
-    "__set_unsubscribed_observer_attribute"
-    (execute___set_attr PredSymb.Aunsubscribed_observer)
-let __split_get_nth = Builtin.register
-    (* splits a string given a separator and returns the nth string *)
-    "__split_get_nth" execute___split_get_nth
-let _ = Builtin.register
-    (* set a hidden field in the struct to the given value *)
-    "__set_hidden_field" execute___set_hidden_field
-let _ = Builtin.register
-    (* set the attribute of the parameter as tainted *)
-    "__set_taint_attribute" execute___set_taint_attribute
-let _ = Builtin.register
-    (* set the attribute of the parameter as untainted *)
-    "__set_untaint_attribute" execute___set_untaint_attribute
-let __set_locked_attribute = Builtin.register
-    (* set the attribute of the parameter as locked *)
-    "__set_locked_attribute" execute___set_locked_attribute
-let __set_unlocked_attribute = Builtin.register
-    (* set the attribute of the parameter as unlocked *)
-    "__set_unlocked_attribute" execute___set_unlocked_attribute
-let __delete_locked_attribute = Builtin.register
-    (* delete the locked attribute, when it exists *)
-    "__delete_locked_attribute" execute___delete_locked_attribute
-let objc_cpp_throw = Builtin.register
-    (* model throwing exception in objc/c++ as divergence *)
-    "__infer_objc_cpp_throw" execute_exit
-let _ = Builtin.register
-    "__throw" execute_skip
-let __unwrap_exception = Builtin.register
-    (* unwrap an exception *)
-    "__unwrap_exception" execute__unwrap_exception
-let _ = Builtin.register
-    (* abort from C library *)
-    "abort" execute_abort
-let _ = Builtin.register
-    (* exit from C library *)
-    "exit" execute_exit
-let _ = Builtin.register
-    (* free from C library, requires allocated memory *)
-    "free" (execute_free PredSymb.Mmalloc)
-let _ = Builtin.register
-    (* fscanf from C library *)
-    "fscanf" (execute_scan_function 2)
-let _ = Builtin.register
-    (* vsscanf from C library *)
-    "fwscanf" (execute_scan_function 2)
-let _ = Builtin.register
-    (* malloc from C library *)
-    "malloc" (execute_alloc PredSymb.Mmalloc (not Config.unsafe_malloc))
-let malloc_no_fail = Builtin.register
-    (* malloc from ObjC library *)
-    "malloc_no_fail" (execute_alloc PredSymb.Mmalloc false)
-let _ = Builtin.register
-    (* register execution handler for pthread_create *)
-    "pthread_create" execute_pthread_create
-let _ = Builtin.register
-    (* scanf from C library *)
-    "scanf" (execute_scan_function 1)
-let _ = Builtin.register
-    (* sscanf from C library *)
-    "sscanf" (execute_scan_function 2)
-let _ = Builtin.register
-    (* vsscanf from C library *)
-    "swscanf" (execute_scan_function 2)
-let _ = Builtin.register
-    (* vfwscanf from C library *)
-    "vfscanf" (execute_scan_function 2)
-let _ = Builtin.register
-    (* vsscanf from C library *)
-    "vfwscanf" (execute_scan_function 2)
-let _ = Builtin.register
-    (* vscanf from C library *)
-    "vscanf" (execute_scan_function 1)
-let _ = Builtin.register
-    (* vsscanf from C library *)
-    "vsscanf" (execute_scan_function 2)
-let _ = Builtin.register
-    (* vsscanf from C library *)
-    "vswscanf" (execute_scan_function 2)
-let _ = Builtin.register
-    (* vsscanf from C library *)
-    "vwscanf" (execute_scan_function 1)
-let _ = Builtin.register
-    (* vsscanf from C library *)
-    "wscanf" (execute_scan_function 1)
-
 let execute_objc_alloc_no_fail
     symb_state typ alloc_fun_opt
     { Builtin.pdesc; tenv; ret_id; loc; } =
-  let alloc_fun = Exp.Const (Const.Cfun __objc_alloc_no_fail) in
+  let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.__objc_alloc_no_fail) in
   let ptr_typ = Typ.Tptr (typ, Typ.Pk_pointer) in
   let sizeof_typ = Exp.Sizeof (typ, None, Subtype.exact) in
   let alloc_fun_exp =
@@ -1153,17 +958,7 @@ let execute_objc_alloc_no_fail
       (ret_id, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default) in
   SymExec.instrs tenv pdesc [alloc_instr] symb_state
 
-let mk_objc_class_method class_name method_name =
-  let method_kind = Procname.ObjCClassMethod in
-  (Procname.ObjC_Cpp
-     (Procname.objc_cpp class_name method_name method_kind))
-
 (* NSArray models *)
-
-let arrayWithObjects_pname = mk_objc_class_method "NSArray" "arrayWithObjects:"
-
-let arrayWithObjectsCount_pname = mk_objc_class_method "NSArray" "arrayWithObjects:count:"
-
 let execute_objc_NSArray_alloc_no_fail builtin_args symb_state pname =
   let ret_typ =
     match builtin_args.Builtin.ret_id with
@@ -1174,19 +969,15 @@ let execute_objc_NSArray_alloc_no_fail builtin_args symb_state pname =
 let execute_NSArray_arrayWithObjects_count builtin_args =
   let n_formals = 1 in
   let res = SymExec.check_variadic_sentinel ~fails_on_nil: true n_formals (0,1) builtin_args in
-  execute_objc_NSArray_alloc_no_fail builtin_args res arrayWithObjectsCount_pname
+  execute_objc_NSArray_alloc_no_fail builtin_args res BuiltinDecl.nsArray_arrayWithObjectsCount
 
 let execute_NSArray_arrayWithObjects builtin_args =
   let n_formals = 1 in
   let res = SymExec.check_variadic_sentinel n_formals (0,1) builtin_args in
-  execute_objc_NSArray_alloc_no_fail builtin_args res arrayWithObjects_pname
+  execute_objc_NSArray_alloc_no_fail builtin_args res BuiltinDecl.nsArray_arrayWithObjects
 
-let _ =
-  Builtin.register_procname arrayWithObjectsCount_pname execute_NSArray_arrayWithObjects_count;
-  Builtin.register_procname arrayWithObjects_pname execute_NSArray_arrayWithObjects
 
 (* NSDictionary models *)
-
 let execute_objc_NSDictionary_alloc_no_fail symb_state pname builtin_args =
   let ret_typ =
     match builtin_args.Builtin.ret_id with
@@ -1194,16 +985,186 @@ let execute_objc_NSDictionary_alloc_no_fail symb_state pname builtin_args =
     | None -> Typ.Tptr (Tvoid, Pk_pointer) in
   execute_objc_alloc_no_fail symb_state ret_typ (Some pname) builtin_args
 
-let __objc_dictionary_literal_pname =
-  mk_objc_class_method "NSDictionary" "dictionaryWithObjects:forKeys:count:"
-
 let execute___objc_dictionary_literal builtin_args =
   let n_formals = 1 in
   let res' = SymExec.check_variadic_sentinel ~fails_on_nil: true n_formals (0,1) builtin_args in
-  let pname = __objc_dictionary_literal_pname in
+  let pname = BuiltinDecl.__objc_dictionary_literal in
   execute_objc_NSDictionary_alloc_no_fail res' pname builtin_args
 
-let __objc_dictionary_literal =
-  let pname = __objc_dictionary_literal_pname in
-  Builtin.register_procname pname execute___objc_dictionary_literal;
-  pname
+let __assert_fail = Builtin.register BuiltinDecl.__assert_fail execute___assert_fail
+
+let __builtin_va_arg = Builtin.register BuiltinDecl.__builtin_va_arg execute___builtin_va_arg
+
+let __builtin_va_copy = Builtin.register BuiltinDecl.__builtin_va_copy execute_skip
+
+let __builtin_va_end = Builtin.register BuiltinDecl.__builtin_va_end execute_skip
+
+let __builtin_va_start = Builtin.register BuiltinDecl.__builtin_va_start execute_skip
+
+(* [__cast(val,typ)] implements java's [typ(val)] *)
+let __cast = Builtin.register BuiltinDecl.__cast execute___cast
+
+(* report a taint error if the parameter is tainted, and assume it is untainted afterward *)
+let __check_untainted = Builtin.register BuiltinDecl.__check_untainted execute___check_untainted
+
+let __cxx_typeid = Builtin.register BuiltinDecl.__cxx_typeid execute___cxx_typeid
+
+let __delete = Builtin.register BuiltinDecl.__delete (execute_free PredSymb.Mnew)
+
+let __delete_array = Builtin.register BuiltinDecl.__delete_array
+    (execute_free PredSymb.Mnew_array)
+
+let __delete_locked_attribute = Builtin.register BuiltinDecl.__delete_locked_attribute
+    execute___delete_locked_attribute
+
+let __exit = Builtin.register BuiltinDecl.__exit execute_exit
+
+(* return the length of the array passed as a parameter *)
+let __get_array_length = Builtin.register BuiltinDecl.__get_array_length execute___get_array_length
+
+let __get_hidden_field = Builtin.register BuiltinDecl.__get_hidden_field execute___get_hidden_field
+
+let __get_type_of = Builtin.register BuiltinDecl.__get_type_of execute___get_type_of
+
+(* infer assume, diverging on inconsistencies *)
+let __infer_assume = Builtin.register BuiltinDecl.__infer_assume execute___infer_assume
+
+(* externally create new errors *)
+let __infer_fail = Builtin.register BuiltinDecl.__infer_fail execute___infer_fail
+
+(* [__instanceof(val,typ)] implements java's [val instanceof typ] *)
+let __instanceof = Builtin.register BuiltinDecl.__instanceof execute___instanceof
+
+let __method_set_ignore_attribute = Builtin.register BuiltinDecl.__method_set_ignore_attribute
+    execute___method_set_ignore_attribute
+
+let __new = Builtin.register BuiltinDecl.__new (execute_alloc PredSymb.Mnew false)
+
+let __new_array = Builtin.register BuiltinDecl.__new_array (execute_alloc PredSymb.Mnew_array false)
+
+let __objc_alloc = Builtin.register BuiltinDecl.__objc_alloc (execute_alloc PredSymb.Mobjc true)
+
+(* like __objc_alloc, but does not return nil *)
+let __objc_alloc_no_fail = Builtin.register BuiltinDecl.__objc_alloc_no_fail
+    (execute_alloc PredSymb.Mobjc false)
+
+let __objc_cast = Builtin.register BuiltinDecl.__objc_cast execute___objc_cast
+
+let __objc_dictionary_literal = Builtin.register BuiltinDecl.__objc_dictionary_literal
+    execute___objc_dictionary_literal
+
+let __objc_release = Builtin.register BuiltinDecl.__objc_release execute___objc_release
+
+let __objc_release_autorelease_pool = Builtin.register BuiltinDecl.__objc_release_autorelease_pool
+    execute___release_autorelease_pool
+
+let __objc_release_cf = Builtin.register BuiltinDecl.__objc_release_cf execute___objc_release_cf
+
+let __objc_retain = Builtin.register BuiltinDecl.__objc_retain execute___objc_retain
+
+let __objc_retain_cf = Builtin.register BuiltinDecl.__objc_retain_cf execute___objc_retain_cf
+
+let __placement_delete = Builtin.register BuiltinDecl.__placement_delete execute_skip
+
+let __placement_new = Builtin.register BuiltinDecl.__placement_new execute_return_first_argument
+
+(* print a value as seen by the engine *)
+let __print_value = Builtin.register BuiltinDecl.__print_value execute___print_value
+
+(* require the parameter to point to an allocated array *)
+let __require_allocated_array = Builtin.register BuiltinDecl.__require_allocated_array
+    execute___require_allocated_array
+
+let __set_array_length = Builtin.register BuiltinDecl.__set_array_length execute___set_array_length
+
+let __set_autorelease_attribute = Builtin.register BuiltinDecl.__set_autorelease_attribute
+    execute___set_autorelease_attribute
+
+let __set_file_attribute = Builtin.register BuiltinDecl.__set_file_attribute
+    execute___set_file_attribute
+
+(* set a hidden field in the struct to the given value *)
+let __set_hidden_field = Builtin.register BuiltinDecl.__set_hidden_field execute___set_hidden_field
+
+let __set_lock_attribute = Builtin.register BuiltinDecl.__set_lock_attribute
+    execute___set_lock_attribute
+
+let __set_locked_attribute = Builtin.register BuiltinDecl.__set_locked_attribute
+    execute___set_locked_attribute
+
+let __set_mem_attribute = Builtin.register BuiltinDecl.__set_mem_attribute
+    execute___set_mem_attribute
+
+let __set_observer_attribute = Builtin.register BuiltinDecl.__set_observer_attribute
+    (execute___set_attr PredSymb.Aobserver)
+
+let __set_taint_attribute = Builtin.register BuiltinDecl.__set_taint_attribute
+    execute___set_taint_attribute
+
+let __set_unlocked_attribute = Builtin.register BuiltinDecl.__set_unlocked_attribute
+    execute___set_unlocked_attribute
+
+let __set_unsubscribed_observer_attribute = Builtin.register
+    BuiltinDecl.__set_unsubscribed_observer_attribute
+    (execute___set_attr PredSymb.Aunsubscribed_observer)
+
+let __set_untaint_attribute = Builtin.register
+    BuiltinDecl.__set_untaint_attribute execute___set_untaint_attribute
+
+(* splits a string given a separator and returns the nth string *)
+let __split_get_nth = Builtin.register BuiltinDecl.__split_get_nth execute___split_get_nth
+
+let __throw = Builtin.register BuiltinDecl.__throw execute_skip
+
+let __unwrap_exception = Builtin.register BuiltinDecl.__unwrap_exception execute__unwrap_exception
+
+let abort = Builtin.register BuiltinDecl.abort execute_abort
+
+let exit = Builtin.register BuiltinDecl.exit execute_exit
+
+let free = Builtin.register BuiltinDecl.free (execute_free PredSymb.Mmalloc)
+
+let fscanf = Builtin.register BuiltinDecl.fscanf (execute_scan_function 2)
+
+let fwscanf = Builtin.register BuiltinDecl.fwscanf (execute_scan_function 2)
+
+let malloc = Builtin.register BuiltinDecl.malloc (execute_alloc PredSymb.Mmalloc
+                                                    (not Config.unsafe_malloc))
+
+let malloc_no_fail = Builtin.register BuiltinDecl.malloc_no_fail
+    (execute_alloc PredSymb.Mmalloc false)
+
+let nsArray_arrayWithObjects = Builtin.register BuiltinDecl.nsArray_arrayWithObjects
+    execute_NSArray_arrayWithObjects
+
+let nsArray_arrayWithObjectsCount = Builtin.register BuiltinDecl.nsArray_arrayWithObjectsCount
+    execute_NSArray_arrayWithObjects_count
+
+(* model throwing exception in objc/c++ as divergence *)
+let objc_cpp_throw = Builtin.register BuiltinDecl.objc_cpp_throw execute_exit
+
+let pthread_create = Builtin.register BuiltinDecl.pthread_create execute_pthread_create
+
+let scanf = Builtin.register BuiltinDecl.scanf (execute_scan_function 1)
+
+let sscanf = Builtin.register BuiltinDecl.sscanf (execute_scan_function 2)
+
+let swscanf = Builtin.register BuiltinDecl.swscanf (execute_scan_function 2)
+
+let vfscanf = Builtin.register BuiltinDecl.vfscanf (execute_scan_function 2)
+
+let vfwscanf = Builtin.register BuiltinDecl.vfwscanf (execute_scan_function 2)
+
+let vscanf = Builtin.register BuiltinDecl.vscanf (execute_scan_function 1)
+
+let vsscanf = Builtin.register BuiltinDecl.vsscanf (execute_scan_function 2)
+
+let vswscanf = Builtin.register BuiltinDecl.vswscanf (execute_scan_function 2)
+
+let vwscanf = Builtin.register BuiltinDecl.vwscanf (execute_scan_function 1)
+
+let wscanf = Builtin.register BuiltinDecl.wscanf (execute_scan_function 1)
+
+(* Function exists to load module and guarantee that the side-effects of Builtin.register
+   calls have been done. *)
+let init () = ()
diff --git a/infer/src/backend/BuiltinDefn.mli b/infer/src/backend/BuiltinDefn.mli
new file mode 100644
index 000000000..43583c1b9
--- /dev/null
+++ b/infer/src/backend/BuiltinDefn.mli
@@ -0,0 +1,18 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! Utils
+
+(** Models for the builtin functions supported *)
+include BUILTINS.S with type t = Builtin.registered
+
+(** Clients of Builtin module should call this before Builtin module is used.
+    WARNING: builtins are not guaranteed to be registered with the Builtin module
+    until after init has been called. *)
+val init : unit -> unit
diff --git a/infer/src/backend/InferAnalyze.re b/infer/src/backend/InferAnalyze.re
index 8714cd08c..242b33215 100644
--- a/infer/src/backend/InferAnalyze.re
+++ b/infer/src/backend/InferAnalyze.re
@@ -127,6 +127,7 @@ let register_perf_stats_report () => {
 
 let () = {
   register_perf_stats_report ();
+  BuiltinDefn.init ();
   if Config.developer_mode {
     Printexc.record_backtrace true
   };
diff --git a/infer/src/backend/builtin.ml b/infer/src/backend/builtin.ml
index 67b57af69..34eef23ae 100644
--- a/infer/src/backend/builtin.ml
+++ b/infer/src/backend/builtin.ml
@@ -27,27 +27,30 @@ type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list
 
 type t = args -> ret_typ
 
+type registered = t
+
 (** builtin function names for which we do symbolic execution *)
 let builtin_functions = Procname.Hash.create 4
 
+let check_register_populated () =
+  (* check if BuiltinDefn were loaded before accessing register *)
+  if Procname.Hash.length builtin_functions = 0 then
+    failwith "Builtins were not initialized"
+  else ()
+
 (** check if the function is a builtin *)
 let is_registered name =
-  Procname.Hash.mem builtin_functions name
+  Procname.Hash.mem builtin_functions name || (check_register_populated (); false)
 
 (** get the symbolic execution handler associated to the builtin function name *)
-let get name : t =
-  try Procname.Hash.find builtin_functions name
-  with Not_found -> assert false
-
-(** register a builtin function name and symbolic execution handler *)
-let register proc_name_str (sym_exe_fun: t) =
-  let proc_name = Procname.from_string_c_fun proc_name_str in
-  Procname.Hash.replace builtin_functions proc_name sym_exe_fun;
-  proc_name
+let get name : t option =
+  try Some (Procname.Hash.find builtin_functions name)
+  with Not_found -> (check_register_populated (); None)
 
 (** register a builtin [Procname.t] and symbolic execution handler *)
-let register_procname proc_name (sym_exe_fun: t) =
-  Procname.Hash.replace builtin_functions proc_name sym_exe_fun
+let register proc_name sym_exe_fun : registered =
+  Procname.Hash.replace builtin_functions proc_name sym_exe_fun;
+  sym_exe_fun
 
 (** print the functions registered *)
 let pp_registered fmt () =
diff --git a/infer/src/backend/builtin.mli b/infer/src/backend/builtin.mli
index 1118754cc..3efbe035f 100644
--- a/infer/src/backend/builtin.mli
+++ b/infer/src/backend/builtin.mli
@@ -27,16 +27,15 @@ type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list
 
 type t = args -> ret_typ
 
-val register : string -> t -> Procname.t
-(** Register a builtin function name and symbolic execution handler *)
+type registered
 
-val register_procname : Procname.t -> t -> unit
+val register : Procname.t -> t -> registered
 (** Register a builtin [Procname.t] and symbolic execution handler *)
 
 val is_registered : Procname.t -> bool
 (** Check if the function is a builtin *)
 
-val get : Procname.t -> t
+val get : Procname.t -> t option
 (** Get the symbolic execution handler associated to the builtin function name *)
 
 val print_and_exit : unit -> 'a
diff --git a/infer/src/backend/inferconfig.ml b/infer/src/backend/inferconfig.ml
index 822642b59..9ffe8407d 100644
--- a/infer/src/backend/inferconfig.ml
+++ b/infer/src/backend/inferconfig.ml
@@ -54,7 +54,7 @@ let is_matching patterns =
 
 (** Check if a proc name is matching the name given as string. *)
 let match_method language proc_name method_name =
-  not (Builtin.is_registered proc_name) &&
+  not (BuiltinDecl.is_declared proc_name) &&
   Procname.get_language proc_name = language &&
   Procname.get_method proc_name = method_name
 
diff --git a/infer/src/backend/modelBuiltins.mli b/infer/src/backend/modelBuiltins.mli
deleted file mode 100644
index cbb36ea05..000000000
--- a/infer/src/backend/modelBuiltins.mli
+++ /dev/null
@@ -1,49 +0,0 @@
-(*
- * Copyright (c) 2016 - present Facebook, Inc.
- * All rights reserved.
- *
- * This source code is licensed under the BSD style license found in the
- * LICENSE file in the root directory of this source tree. An additional grant
- * of patent rights can be found in the PATENTS file in the same directory.
- *)
-
-open! Utils
-
-(** Models for the builtin functions supported *)
-
-val __assert_fail : Procname.t
-val __delete : Procname.t
-val __delete_array : Procname.t
-val __exit : Procname.t
-val __get_array_length : Procname.t
-val __get_type_of : Procname.t
-val __infer_fail : Procname.t
-val __instanceof : Procname.t (** [__instanceof(val,typ)] implements java's [val instanceof typ] *)
-
-val __cast : Procname.t (** [__cast(val,typ)] implements java's [typ(val)] *)
-
-val __placement_delete : Procname.t
-val __placement_new : Procname.t
-val __new : Procname.t
-val __new_array : Procname.t
-val __objc_alloc : Procname.t
-val __objc_alloc_no_fail : Procname.t
-val __set_array_length : Procname.t
-val __unwrap_exception : Procname.t
-val __set_file_attribute : Procname.t
-val __set_mem_attribute : Procname.t
-val __set_locked_attribute : Procname.t
-val __set_unlocked_attribute : Procname.t
-val __delete_locked_attribute : Procname.t
-val __infer_assume : Procname.t
-val __objc_retain : Procname.t
-val __objc_release : Procname.t
-val __objc_retain_cf : Procname.t
-val __objc_release_cf : Procname.t
-val __set_autorelease_attribute : Procname.t
-val __objc_release_autorelease_pool : Procname.t
-val __objc_cast : Procname.t
-val __objc_dictionary_literal : Procname.t
-val __cxx_typeid : Procname.t
-val malloc_no_fail : Procname.t
-val objc_cpp_throw : Procname.t
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 52b2f8427..4f5e9d0cf 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -1054,7 +1054,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
       ret_old_path (Propset.to_proplist (prune tenv ~positive:true n_cond prop))
   | Sil.Call (ret_id, Exp.Const (Const.Cfun callee_pname), args, loc, _)
     when Builtin.is_registered callee_pname ->
-      let sym_exe_builtin = Builtin.get callee_pname in
+      let sym_exe_builtin =  Option.get (Builtin.get callee_pname) in
       sym_exe_builtin (call_args prop_ callee_pname args ret_id loc)
   | Sil.Call (ret_id,
               Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml
index b700ec4b6..e4ad8fa2e 100644
--- a/infer/src/checkers/ThreadSafety.ml
+++ b/infer/src/checkers/ThreadSafety.ml
@@ -33,9 +33,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module Domain = CombinedDomain
   type extras = ProcData.no_extras
 
-  let is_lock_procedure pn = Procname.equal pn ModelBuiltins.__set_locked_attribute
+  let is_lock_procedure pn = Procname.equal pn BuiltinDecl.__set_locked_attribute
 
-  let is_unlock_procedure pn = Procname.equal pn ModelBuiltins.__delete_locked_attribute
+  let is_unlock_procedure pn = Procname.equal pn BuiltinDecl.__delete_locked_attribute
 
   let add_path_to_state exp typ pathdomainstate =
     IList.fold_left
diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml
index b721f68e1..709835b8d 100644
--- a/infer/src/checkers/annotationReachability.ml
+++ b/infer/src/checkers/annotationReachability.ml
@@ -112,7 +112,7 @@ let annotation_reachability_error = "CHECKERS_ANNOTATION_REACHABILITY_ERROR"
 
 let is_modeled_expensive tenv = function
   | Procname.Java proc_name_java as proc_name ->
-      not (Builtin.is_registered proc_name) &&
+      not (BuiltinDecl.is_declared proc_name) &&
       let is_subclass =
         let classname = Typename.Java.from_string (Procname.java_get_class_name proc_name_java) in
         PatternMatch.is_subtype_of_str tenv classname in
@@ -128,7 +128,7 @@ let is_allocator tenv pname =
           Typename.Java.from_string (Procname.java_get_class_name pname_java) in
         PatternMatch.is_throwable tenv class_name in
       Procname.is_constructor pname
-      && not (Builtin.is_registered pname)
+      && not (BuiltinDecl.is_declared pname)
       && not (is_throwable ())
   | _ ->
       false
diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml
index 7fe7f893a..8fc0e6b0b 100644
--- a/infer/src/checkers/dataflow.ml
+++ b/infer/src/checkers/dataflow.ml
@@ -58,8 +58,8 @@ let node_throws node (proc_throws : Procname.t -> throws) : throws =
         (* assignment to return variable is an artifact of a throw instruction *)
         Throws
     | Sil.Call (_, Exp.Const (Const.Cfun callee_pn), _, _, _)
-      when Builtin.is_registered callee_pn ->
-        if Procname.equal callee_pn ModelBuiltins.__cast
+      when BuiltinDecl.is_declared callee_pn ->
+        if Procname.equal callee_pn BuiltinDecl.__cast
         then DontKnow
         else DoesNotThrow
     | Sil.Call (_, Exp.Const (Const.Cfun callee_pn), _, _, _) ->
diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml
index eb041c91e..e7a8b38f7 100644
--- a/infer/src/checkers/repeatedCallsChecker.ml
+++ b/infer/src/checkers/repeatedCallsChecker.ml
@@ -66,8 +66,8 @@ struct
     let node_allocates node : Location.t option =
       let found = ref None in
       let proc_is_new pn =
-        Procname.equal pn ModelBuiltins.__new ||
-        Procname.equal pn ModelBuiltins.__new_array in
+        Procname.equal pn BuiltinDecl.__new ||
+        Procname.equal pn BuiltinDecl.__new_array in
       let do_instr instr =
         match instr with
         | Sil.Call (_, Exp.Const (Const.Cfun pn), _, loc, _) when proc_is_new pn ->
diff --git a/infer/src/clang/ast_expressions.ml b/infer/src/clang/ast_expressions.ml
index 45c3f88a5..43d8e34d3 100644
--- a/infer/src/clang/ast_expressions.ml
+++ b/infer/src/clang/ast_expressions.ml
@@ -627,6 +627,6 @@ let create_assume_not_null_call decl_info var_name var_type =
   let bin_op_expr_info = make_general_expr_info create_BOOL_type `RValue `Ordinary in
   let bin_op = make_binary_stmt decl_ref_exp_cast null_expr stmt_info bin_op_expr_info boi in
   let parameters = [bin_op] in
-  let procname = Procname.to_string ModelBuiltins.__infer_assume in
+  let procname = Procname.to_string BuiltinDecl.__infer_assume in
   let qual_procname = Ast_utils.make_name_decl procname in
   create_call stmt_info var_decl_ptr qual_procname create_void_star_type parameters
diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml
index f272e4cc2..6f56b30f1 100644
--- a/infer/src/clang/cArithmetic_trans.ml
+++ b/infer/src/clang/cArithmetic_trans.ml
@@ -22,9 +22,9 @@ open CFrontend_utils
 (* See document: "Objective-C Automatic Reference Counting" describing the semantics *)
 let assignment_arc_mode e1 typ e2 loc rhs_owning_method is_e1_decl =
   let assign = Sil.Store (e1, typ, e2, loc) in
-  let retain_pname = ModelBuiltins.__objc_retain in
-  let release_pname = ModelBuiltins.__objc_release in
-  let autorelease_pname = ModelBuiltins.__set_autorelease_attribute in
+  let retain_pname = BuiltinDecl.__objc_retain in
+  let release_pname = BuiltinDecl.__objc_release in
+  let autorelease_pname = BuiltinDecl.__set_autorelease_attribute in
   let mk_call procname e t =
     let bi_retain = Exp.Const (Const.Cfun procname) in
     Sil.Call (None, bi_retain, [(e, t)], loc, CallFlags.default) in
diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml
index 7b50c019f..4ac0b7390 100644
--- a/infer/src/clang/cTrans.ml
+++ b/infer/src/clang/cTrans.ml
@@ -73,7 +73,7 @@ struct
     if !Config.arc_mode &&
        not (CTrans_utils.is_owning_name method_name) &&
        ObjcInterface_decl.is_pointer_to_objc_class typ then
-      let fname = ModelBuiltins.__set_autorelease_attribute in
+      let fname = BuiltinDecl.__set_autorelease_attribute in
       let ret_id = Some (Ident.create_fresh Ident.knormal, Typ.Tvoid) in
       (* TODO(jjb): change ret_id to None? *)
       let stmt_call =
@@ -445,12 +445,12 @@ struct
     | _ when CTrans_models.is_modeled_builtin name ->
         Some (Procname.from_string_c_fun (CFrontend_config.infer ^ name))
     | _ when CTrans_models.is_release_builtin name type_ptr ->
-        Some ModelBuiltins.__objc_release_cf
+        Some BuiltinDecl.__objc_release_cf
     | _ when CTrans_models.is_retain_builtin name type_ptr ->
-        Some ModelBuiltins.__objc_retain_cf
+        Some BuiltinDecl.__objc_retain_cf
     | _ when name = CFrontend_config.malloc &&
              General_utils.is_objc_extension trans_unit_ctx ->
-        Some ModelBuiltins.malloc_no_fail
+        Some BuiltinDecl.malloc_no_fail
     | _ -> None
 
 
@@ -1961,7 +1961,7 @@ struct
     let typ =
       CTypes_decl.class_from_pointer_type
         trans_state.context.CContext.tenv info.Clang_ast_t.ei_type_ptr in
-    let dictionary_literal_pname = ModelBuiltins.__objc_dictionary_literal in
+    let dictionary_literal_pname = BuiltinDecl.__objc_dictionary_literal in
     let dictionary_literal_s = Procname.get_method dictionary_literal_pname in
     let obj_c_message_expr_info =
       Ast_expressions.make_obj_c_message_expr_info_class dictionary_literal_s typ None in
@@ -1989,7 +1989,7 @@ struct
   and objcAutoreleasePool_trans trans_state stmt_info stmts =
     let context = trans_state.context in
     let sil_loc = CLocation.get_sil_location stmt_info context in
-    let fname = ModelBuiltins.__objc_release_autorelease_pool in
+    let fname = BuiltinDecl.__objc_release_autorelease_pool in
     let ret_id = Some (Ident.create_fresh Ident.knormal, Typ.Tvoid) in
     (* TODO(jjb): change ret_id to None? *)
     let autorelease_pool_vars = CVar_decl.compute_autorelease_pool_vars context stmts in
@@ -2148,8 +2148,8 @@ struct
     let sil_loc = CLocation.get_sil_location stmt_info context in
     let is_array = delete_expr_info.Clang_ast_t.xdei_is_array in
     let fname =
-      if is_array then ModelBuiltins.__delete_array
-      else ModelBuiltins.__delete in
+      if is_array then BuiltinDecl.__delete_array
+      else BuiltinDecl.__delete in
     let param = match stmt_list with [p] -> p | _ -> assert false 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
@@ -2211,7 +2211,7 @@ struct
     let sizeof_expr = match cast_type with
       | Typ.Tptr (typ, _) -> Exp.Sizeof (typ, None, subtypes)
       | _ -> assert false in
-    let builtin = Exp.Const (Const.Cfun ModelBuiltins.__cast) in
+    let builtin = Exp.Const (Const.Cfun BuiltinDecl.__cast) in
     let stmt = match stmts with [stmt] -> stmt | _ -> assert false in
     let res_trans_stmt = exec_with_glvalue_as_reference instruction trans_state' stmt in
     let exp = match res_trans_stmt.exps with | [e] -> e | _ -> assert false in
@@ -2252,7 +2252,7 @@ struct
     let pname = Procname.from_string_c_fun CFrontend_config.infer_skip_gcc_asm_stmt in
     call_function_with_args "GCCAsmStmt" pname trans_state
   and objc_cxx_throw_trans trans_state =
-    call_function_with_args "ObjCCPPThrow" ModelBuiltins.objc_cpp_throw trans_state
+    call_function_with_args "ObjCCPPThrow" BuiltinDecl.objc_cpp_throw trans_state
 
   and cxxPseudoDestructorExpr_trans () =
     let fun_name = Procname.from_string_c_fun CFrontend_config.infer_skip_fun in
@@ -2269,7 +2269,7 @@ struct
           let trans_state_param = { trans_state_pri with succ_nodes = [] } in
           instruction trans_state_param stmt
       | _ -> empty_res_trans in
-    let fun_name = ModelBuiltins.__cxx_typeid in
+    let fun_name = BuiltinDecl.__cxx_typeid in
     let sil_fun = Exp.Const (Const.Cfun fun_name) in
     let ret_id = Ident.create_fresh Ident.knormal in
     let type_info_objc = (Exp.Sizeof (typ, None, Subtype.exact), Typ.Tvoid) in
diff --git a/infer/src/clang/cTrans_models.ml b/infer/src/clang/cTrans_models.ml
index 6bd01ee4f..73171e40e 100644
--- a/infer/src/clang/cTrans_models.ml
+++ b/infer/src/clang/cTrans_models.ml
@@ -56,11 +56,11 @@ let is_autorelease_method funct =
 
 let get_builtinname method_name =
   if is_retain_method method_name then
-    Some ModelBuiltins.__objc_retain
+    Some BuiltinDecl.__objc_retain
   else if is_autorelease_method method_name then
-    Some ModelBuiltins.__set_autorelease_attribute
+    Some BuiltinDecl.__set_autorelease_attribute
   else if is_release_method method_name then
-    Some ModelBuiltins.__objc_release
+    Some BuiltinDecl.__objc_release
   else None
 
 let is_modeled_builtin funct =
@@ -115,8 +115,8 @@ let is_toll_free_bridging pn =
   funct = CFrontend_config.ns_make_collectable
 
 let is_cf_retain_release pn =
-  Procname.equal pn ModelBuiltins.__objc_retain_cf
-  || Procname.equal pn ModelBuiltins.__objc_release_cf
+  Procname.equal pn BuiltinDecl.__objc_retain_cf
+  || Procname.equal pn BuiltinDecl.__objc_release_cf
 
 (** If the function is a builtin model, return the model, otherwise return the function *)
 let is_assert_log pname =
@@ -180,7 +180,7 @@ let get_predefined_ms_nsautoreleasepool_release class_name method_name mk_procna
   let args = [(Mangled.from_string CFrontend_config.self, class_type)] in
   get_predefined_ms_method condition class_name method_name Procname.ObjCInstanceMethod
     mk_procname lang args Ast_expressions.create_void_type
-    [] (Some ModelBuiltins.__objc_release_autorelease_pool)
+    [] (Some BuiltinDecl.__objc_release_autorelease_pool)
 
 let get_predefined_ms_is_kind_of_class class_name method_name mk_procname lang =
   let condition = method_name = CFrontend_config.is_kind_of_class in
@@ -188,7 +188,7 @@ let get_predefined_ms_is_kind_of_class class_name method_name mk_procname lang =
   let args = [(Mangled.from_string CFrontend_config.self, class_type)] in
   get_predefined_ms_method condition class_name method_name Procname.ObjCInstanceMethod
     mk_procname lang args Ast_expressions.create_BOOL_type
-    [] (Some ModelBuiltins.__instanceof)
+    [] (Some BuiltinDecl.__instanceof)
 
 let get_predefined_model_method_signature class_name method_name mk_procname lang =
   let next_predefined f = function
diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml
index e446b7b68..3af8ef6d2 100644
--- a/infer/src/clang/cTrans_utils.ml
+++ b/infer/src/clang/cTrans_utils.ml
@@ -313,9 +313,9 @@ let create_alloc_instrs sil_loc function_type fname size_exp_opt procname_opt =
 
 let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc procname_opt =
   let fname = if is_cf_non_null_alloc then
-      ModelBuiltins.__objc_alloc_no_fail
+      BuiltinDecl.__objc_alloc_no_fail
     else
-      ModelBuiltins.__objc_alloc in
+      BuiltinDecl.__objc_alloc in
   let (function_type, stmt_call, exp) =
     create_alloc_instrs loc function_type fname None procname_opt in
   let res_trans_tmp = { empty_res_trans with instrs =[stmt_call]} in
@@ -325,7 +325,7 @@ let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc pro
   { res_trans with exps =[(exp, function_type)]}
 
 let objc_new_trans trans_state loc stmt_info cls_name function_type =
-  let fname = ModelBuiltins.__objc_alloc_no_fail in
+  let fname = BuiltinDecl.__objc_alloc_no_fail in
   let (alloc_ret_type, alloc_stmt_call, alloc_ret_exp) =
     create_alloc_instrs loc function_type fname None None in
   let init_ret_id = Ident.create_fresh Ident.knormal in
@@ -362,8 +362,8 @@ let new_or_alloc_trans trans_state loc stmt_info type_ptr class_name_opt selecto
 let cpp_new_trans sil_loc function_type size_exp_opt =
   let fname =
     match size_exp_opt with
-    | Some _ -> ModelBuiltins.__new_array
-    | None -> ModelBuiltins.__new in
+    | Some _ -> BuiltinDecl.__new_array
+    | None -> BuiltinDecl.__new in
   let (function_type, stmt_call, exp) =
     create_alloc_instrs sil_loc function_type fname size_exp_opt None in
   { empty_res_trans with instrs = [stmt_call]; exps = [(exp, function_type)] }
@@ -373,7 +373,7 @@ let create_cast_instrs exp cast_from_typ cast_to_typ sil_loc =
   let ret_id_typ = Some (ret_id, cast_to_typ) in
   let typ = CTypes.remove_pointer_to_typ cast_to_typ in
   let sizeof_exp = Exp.Sizeof (typ, None, Subtype.exact) in
-  let pname = ModelBuiltins.__objc_cast in
+  let pname = BuiltinDecl.__objc_cast in
   let args = [(exp, cast_from_typ); (sizeof_exp, Typ.Tint Typ.IULong)] in
   let stmt_call =
     Sil.Call (ret_id_typ, Exp.Const (Const.Cfun pname), args, sil_loc, CallFlags.default) in
@@ -439,7 +439,7 @@ let cast_operation trans_state cast_kind exps cast_typ sil_loc is_objc_bridged =
       ([], (exp, cast_typ))
 
 let trans_assertion_failure sil_loc context =
-  let assert_fail_builtin = Exp.Const (Const.Cfun ModelBuiltins.__infer_fail) in
+  let assert_fail_builtin = Exp.Const (Const.Cfun BuiltinDecl.__infer_fail) in
   let args = [Exp.Const (Const.Cstr Config.default_failure_name), Typ.Tvoid] in
   let call_instr = Sil.Call (None, assert_fail_builtin, args, sil_loc, CallFlags.default) in
   let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context)
diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml
index f31740585..6835c0bed 100644
--- a/infer/src/eradicate/eradicateChecks.ml
+++ b/infer/src/eradicate/eradicateChecks.ml
@@ -122,7 +122,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname
       | _ -> false in
     let do_instr = function
       | Sil.Call (_, Exp.Const (Const.Cfun pn), [_; (Exp.Sizeof(t, _, _), _)], _, _) when
-          Procname.equal pn ModelBuiltins.__instanceof && typ_is_throwable t ->
+          Procname.equal pn BuiltinDecl.__instanceof && typ_is_throwable t ->
           throwable_found := true
       | _ -> () in
     let do_node n =
diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml
index a74f21341..e2c45d78d 100644
--- a/infer/src/eradicate/typeCheck.ml
+++ b/infer/src/eradicate/typeCheck.ml
@@ -41,7 +41,7 @@ module ComplexExpressions = struct
 
 
   let procname_optional_isPresent = Models.is_optional_isPresent
-  let procname_instanceof = Procname.equal ModelBuiltins.__instanceof
+  let procname_instanceof = Procname.equal BuiltinDecl.__instanceof
 
   let procname_is_false_on_null pn =
     match Specs.proc_resolve_attributes pn with
@@ -73,7 +73,7 @@ module ComplexExpressions = struct
     procname_optional_isPresent pn ||
     procname_instanceof pn ||
     procname_containsKey pn ||
-    Builtin.is_registered pn
+    BuiltinDecl.is_declared pn
 
 
   exception Not_handled
@@ -508,14 +508,14 @@ let typecheck_instr
       check_field_assign ();
       typestate2
   | Sil.Call (Some (id, _), Exp.Const (Const.Cfun pn), [(_, typ)], loc, _)
-    when Procname.equal pn ModelBuiltins.__new ||
-         Procname.equal pn ModelBuiltins.__new_array ->
+    when Procname.equal pn BuiltinDecl.__new ||
+         Procname.equal pn BuiltinDecl.__new_array ->
       TypeState.add_id
         id
         (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.New, [loc])
         typestate (* new never returns null *)
   | Sil.Call (Some (id, _), Exp.Const (Const.Cfun pn), (e, typ):: _, loc, _)
-    when Procname.equal pn ModelBuiltins.__cast ->
+    when Procname.equal pn BuiltinDecl.__cast ->
       typecheck_expr_for_errors typestate e loc;
       let e', typestate' =
         convert_complex_exp_to_pvar node false e typestate loc in
@@ -524,7 +524,7 @@ let typecheck_instr
         (typecheck_expr_simple typestate' e' typ TypeOrigin.ONone loc)
         typestate'
   | Sil.Call (Some (id, _), Exp.Const (Const.Cfun pn), [(array_exp, t)], loc, _)
-    when Procname.equal pn ModelBuiltins.__get_array_length ->
+    when Procname.equal pn BuiltinDecl.__get_array_length ->
       let (_, ta, _) = typecheck_expr
           find_canonical_duplicate
           calls_this
@@ -555,7 +555,7 @@ let typecheck_instr
           [loc]
         )
         typestate
-  | Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when Builtin.is_registered pn ->
+  | Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when BuiltinDecl.is_declared pn ->
       typestate (* skip othe builtins *)
   | Sil.Call
       (ret_id,
diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml
index f72fa5f9c..11d33b024 100644
--- a/infer/src/harness/inhabit.ml
+++ b/infer/src/harness/inhabit.ml
@@ -87,11 +87,11 @@ let rec inhabit_typ tenv typ cfg env =
       | Typ.Tptr (Typ.Tarray (inner_typ, Some _), Typ.Pk_pointer) ->
           let len = Exp.Const (Const.Cint (IntLit.one)) in
           let arr_typ = Typ.Tarray (inner_typ, Some IntLit.one) in
-          inhabit_alloc arr_typ (Some len) typ ModelBuiltins.__new_array env
+          inhabit_alloc arr_typ (Some len) typ BuiltinDecl.__new_array env
       | Typ.Tptr (typ, Typ.Pk_pointer) as ptr_to_typ ->
           (* TODO (t4575417): this case does not work correctly for enums, but they are currently
            * broken in Infer anyway (see t4592290) *)
-          let (allocated_obj_exp, env) = inhabit_alloc typ None typ ModelBuiltins.__new env in
+          let (allocated_obj_exp, env) = inhabit_alloc typ None typ BuiltinDecl.__new env in
           (* select methods that are constructors and won't force us into infinite recursion because
            * we are already inhabiting one of their argument types *)
           let get_all_suitable_constructors (typ: Typ.t) =
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index 18206d61f..78cf3a79b 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -339,10 +339,10 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio
       None
 
 let builtin_new =
-  Exp.Const (Const.Cfun ModelBuiltins.__new)
+  Exp.Const (Const.Cfun BuiltinDecl.__new)
 
 let builtin_get_array_length =
-  Exp.Const (Const.Cfun ModelBuiltins.__get_array_length)
+  Exp.Const (Const.Cfun BuiltinDecl.__get_array_length)
 
 let create_sil_deref exp typ loc =
   let no_id = Ident.create_none () in
@@ -405,8 +405,8 @@ let rec expression (context : JContext.t) pc expr =
               JTransType.sizeof_of_object_type program tenv ot subtypes in
             let builtin =
               (match unop with
-               | JBir.InstanceOf _ -> Exp.Const (Const.Cfun ModelBuiltins.__instanceof)
-               | JBir.Cast _ -> Exp.Const (Const.Cfun ModelBuiltins.__cast)
+               | JBir.InstanceOf _ -> Exp.Const (Const.Cfun BuiltinDecl.__instanceof)
+               | JBir.Cast _ -> Exp.Const (Const.Cfun BuiltinDecl.__cast)
                | _ -> assert false) in
             let args = [(sil_ex, type_of_ex); (sizeof_expr, Typ.Tvoid)] in
             let ret_id = Ident.create_fresh Ident.knormal in
@@ -519,7 +519,7 @@ let method_invocation
   let callee_procname =
     let proc = Procname.from_string_c_fun (JBasics.ms_name ms) in
     if JBasics.cn_equal cn' (JBasics.make_cn JConfig.infer_builtins_cl) &&
-       Builtin.is_registered proc
+       BuiltinDecl.is_declared proc
     then proc
     else Procname.Java (JTransType.get_method_procname cn' ms method_kind) in
   let call_instrs =
@@ -550,7 +550,7 @@ let method_invocation
     | (_, typ) as exp :: _
       when Procname.is_constructor callee_procname && JTransType.is_closeable program tenv typ ->
         let set_file_attr =
-          let set_builtin = Exp.Const (Const.Cfun ModelBuiltins.__set_file_attribute) in
+          let set_builtin = Exp.Const (Const.Cfun BuiltinDecl.__set_file_attribute) in
           Sil.Call (None, set_builtin, [exp], loc, CallFlags.default) in
         (* Exceptions thrown in the constructor should prevent adding the resource attribute *)
         call_instrs @ [set_file_attr]
@@ -559,7 +559,7 @@ let method_invocation
     | (_, typ) as exp :: []
       when Procname.java_is_close callee_procname && JTransType.is_closeable program tenv typ ->
         let set_mem_attr =
-          let set_builtin = Exp.Const (Const.Cfun ModelBuiltins.__set_mem_attribute) in
+          let set_builtin = Exp.Const (Const.Cfun BuiltinDecl.__set_mem_attribute) in
           Sil.Call (None, set_builtin, [exp], loc, CallFlags.default) in
         (* Exceptions thrown in the close method should not prevent the resource from being *)
         (* considered as closed *)
@@ -690,7 +690,7 @@ let is_this expr =
 
 
 let assume_not_null loc sil_expr =
-  let builtin_infer_assume = Exp.Const (Const.Cfun ModelBuiltins.__infer_assume) in
+  let builtin_infer_assume = Exp.Const (Const.Cfun BuiltinDecl.__infer_assume) in
   let not_null_expr =
     Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in
   let assume_call_flag = { CallFlags.default with CallFlags.cf_noreturn = true; } in
@@ -818,7 +818,7 @@ let rec instruction (context : JContext.t) pc instr : translation =
         JContext.add_goto_jump context pc JContext.Exit;
         Instr node
     | JBir.New (var, cn, constr_type_list, constr_arg_list) ->
-        let builtin_new = Exp.Const (Const.Cfun ModelBuiltins.__new) in
+        let builtin_new = Exp.Const (Const.Cfun BuiltinDecl.__new) in
         let class_type = JTransType.get_class_type program tenv cn in
         let class_type_np = JTransType.get_class_type_no_pointer program tenv cn in
         let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in
@@ -840,7 +840,7 @@ let rec instruction (context : JContext.t) pc instr : translation =
         Cg.add_edge cg caller_procname constr_procname;
         Instr node
     | JBir.NewArray (var, vt, expr_list) ->
-        let builtin_new_array = Exp.Const (Const.Cfun ModelBuiltins.__new_array) in
+        let builtin_new_array = Exp.Const (Const.Cfun BuiltinDecl.__new_array) in
         let content_type = JTransType.value_type program tenv vt in
         let array_type = JTransType.create_array_type content_type (IList.length expr_list) in
         let array_name = JContext.set_pvar context var array_type in
@@ -1016,7 +1016,7 @@ let rec instruction (context : JContext.t) pc instr : translation =
         and ret_id = Ident.create_fresh Ident.knormal
         and sizeof_expr =
           JTransType.sizeof_of_object_type program tenv object_type Subtype.subtypes_instof in
-        let check_cast = Exp.Const (Const.Cfun ModelBuiltins.__instanceof) in
+        let check_cast = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in
         let args = [(sil_expr, sil_type); (sizeof_expr, Typ.Tvoid)] in
         let call = Sil.Call (Some (ret_id, ret_type), check_cast, args, loc, CallFlags.default) in
         let res_ex = Exp.Var ret_id in
@@ -1050,11 +1050,11 @@ let rec instruction (context : JContext.t) pc instr : translation =
         Prune (is_instance_node, throw_cast_exception_node)
     | JBir.MonitorEnter expr ->
         trans_monitor_enter_exit
-          context expr pc loc ModelBuiltins.__set_locked_attribute "MonitorEnter"
+          context expr pc loc BuiltinDecl.__set_locked_attribute "MonitorEnter"
 
     | JBir.MonitorExit expr ->
         trans_monitor_enter_exit
-          context expr pc loc ModelBuiltins.__delete_locked_attribute "MonitorExit"
+          context expr pc loc BuiltinDecl.__delete_locked_attribute "MonitorExit"
 
     | _ -> Skip
   with Frontend_error s ->
diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml
index 95db3ca11..fecf5d859 100644
--- a/infer/src/java/jTransExn.ml
+++ b/infer/src/java/jTransExn.ml
@@ -40,7 +40,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
     let instr_get_ret_val = Sil.Load (id_ret_val, Exp.Lvar ret_var, ret_type, loc) in
     let instr_deactivate_exn = Sil.Store (Exp.Lvar ret_var, ret_type, Exp.null, loc) in
     let instr_unwrap_ret_val =
-      let unwrap_builtin = Exp.Const (Const.Cfun ModelBuiltins.__unwrap_exception) in
+      let unwrap_builtin = Exp.Const (Const.Cfun BuiltinDecl.__unwrap_exception) in
       Sil.Call
         (Some (id_exn_val, ret_type), unwrap_builtin, [(Exp.Var id_ret_val, ret_type)], loc,
          CallFlags.default) in
@@ -68,7 +68,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
           | _ -> assert false in
         let id_instanceof = Ident.create_fresh Ident.knormal in
         let instr_call_instanceof =
-          let instanceof_builtin = Exp.Const (Const.Cfun ModelBuiltins.__instanceof) in
+          let instanceof_builtin = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in
           let args = [
             (Exp.Var id_exn_val, Typ.Tptr(exn_type, Typ.Pk_pointer));
             (Exp.Sizeof (exn_type, None, Subtype.exact), Typ.Tvoid)] in
diff --git a/infer/src/quandary/CppTrace.ml b/infer/src/quandary/CppTrace.ml
index 544030ecf..8ca66fe99 100644
--- a/infer/src/quandary/CppTrace.ml
+++ b/infer/src/quandary/CppTrace.ml
@@ -68,7 +68,7 @@ module CppSource = struct
           | "__infer_taint_source" -> Some (make Other site)
           | _ -> None
         end
-    | pname when Builtin.is_registered pname ->
+    | pname when BuiltinDecl.is_declared pname ->
         None
     | pname ->
         failwithf "Non-C++ procname %a in C++ analysis@." Procname.pp pname
@@ -145,7 +145,7 @@ module CppSink = struct
           | _ ->
               []
         end
-    | pname when Builtin.is_registered pname ->
+    | pname when BuiltinDecl.is_declared pname ->
         []
     | pname ->
         failwithf "Non-C++ procname %a in C++ analysis@." Procname.pp pname
diff --git a/infer/src/quandary/JavaTaintAnalysis.ml b/infer/src/quandary/JavaTaintAnalysis.ml
index c08845dd9..856035793 100644
--- a/infer/src/quandary/JavaTaintAnalysis.ml
+++ b/infer/src/quandary/JavaTaintAnalysis.ml
@@ -89,7 +89,7 @@ include
             | _ ->
                 []
           end
-      | pname when Builtin.is_registered pname ->
+      | pname when BuiltinDecl.is_declared pname ->
           []
       | pname ->
           failwithf "Non-Java procname %a in Java analysis@." Procname.pp pname
diff --git a/infer/src/quandary/JavaTrace.ml b/infer/src/quandary/JavaTrace.ml
index 3f0f8970d..da127e2cb 100644
--- a/infer/src/quandary/JavaTrace.ml
+++ b/infer/src/quandary/JavaTrace.ml
@@ -78,7 +78,7 @@ module JavaSource = struct
           | _ ->
               None
         end
-    | pname when Builtin.is_registered pname -> None
+    | pname when BuiltinDecl.is_declared pname -> None
     | pname -> failwithf "Non-Java procname %a in Java analysis@." Procname.pp pname
 
   let compare src1 src2 =
@@ -177,7 +177,7 @@ module JavaSink = struct
           | _ ->
               []
         end
-    | pname when Builtin.is_registered pname -> []
+    | pname when BuiltinDecl.is_declared pname -> []
     | pname -> failwithf "Non-Java procname %a in Java analysis@." Procname.pp pname
 
   let to_callee t callee_site =
diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml
index fe3e020f9..4c2662d4a 100644
--- a/infer/src/quandary/TaintAnalysis.ml
+++ b/infer/src/quandary/TaintAnalysis.ml
@@ -297,8 +297,8 @@ module Make (TaintSpec : TaintSpec.S) = struct
                 astate'
           end
       | Sil.Call (Some (ret_id, _), Const (Cfun callee_pname), args, loc, _)
-        when Builtin.is_registered callee_pname ->
-          if Procname.equal callee_pname ModelBuiltins.__cast
+        when BuiltinDecl.is_declared callee_pname ->
+          if Procname.equal callee_pname BuiltinDecl.__cast
           then
             match args with
             | (cast_target, cast_typ) :: _ ->
diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml
index 96fbcc01a..b9a565395 100644
--- a/infer/src/unit/analyzerTester.ml
+++ b/infer/src/unit/analyzerTester.ml
@@ -124,7 +124,7 @@ module StructuredSil = struct
   let cast_id_to_id lhs cast_typ rhs =
     let lhs_id = ident_of_str lhs in
     let rhs_id = Exp.Var (ident_of_str rhs) in
-    make_call ~procname:ModelBuiltins.__cast (Some (lhs_id, cast_typ)) [rhs_id, cast_typ]
+    make_call ~procname:BuiltinDecl.__cast (Some (lhs_id, cast_typ)) [rhs_id, cast_typ]
 
   let var_assign_exp ~rhs_typ lhs rhs_exp =
     let lhs_exp = var_of_str lhs in