summaryrefslogtreecommitdiff
path: root/compiler/ExtractBuiltin.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/ExtractBuiltin.ml')
-rw-r--r--compiler/ExtractBuiltin.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 2e46b120..9cc7c226 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -29,6 +29,7 @@ module SimpleNameOrd = struct
end
module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
+module SimpleNameSet = Collections.MakeSet (SimpleNameOrd)
(** Small utility to memoize some computations *)
let mk_memoized (f : unit -> 'a) : unit -> 'a =
@@ -374,6 +375,13 @@ let mk_builtin_funs_map () =
let builtin_funs_map = mk_memoized mk_builtin_funs_map
+let builtin_non_fallible_funs =
+ [ "alloc::boxed::Box::deref"; "alloc::boxed::Box::deref_mut" ]
+
+let builtin_non_fallible_funs_set =
+ SimpleNameSet.of_list
+ (List.map string_to_simple_name builtin_non_fallible_funs)
+
type builtin_trait_decl_info = {
rust_name : string;
extract_name : string;