Fix minor issues

AeneasVerif · Nov 20, 2023 · db58a6b · db58a6b
1 parent 5aa37b3
commit db58a6b
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 3 deletions.
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
@@ -8,6 +8,8 @@ open Config
 open Charon.NameMatcher (* TODO: include? *)
 include ExtractName (* TODO: only open? *)
 
+let log = Logging.builtin_log
+
 (** Small utility to memoize some computations *)
 let mk_memoized (f : unit -> 'a) : unit -> 'a =
   let r = ref None in
@@ -492,9 +494,9 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
   in
   [
     (* core::ops::Deref<alloc::boxed::Box<T>> *)
-    fmt "core::ops::Deref<Box<@T>>" ();
-    (* core::ops::Deref<alloc::boxed::Box<T>> *)
-    fmt "core::ops::Deref<Box<@T>>" ();
+    fmt "core::ops::deref::Deref<Box<@T>>" ();
+    (* core::ops::DerefMut<alloc::boxed::Box<T>> *)
+    fmt "core::ops::deref::DerefMut<Box<@T>>" ();
     (* core::ops::index::Index<[T], I> *)
     fmt "core::ops::index::Index<[@T], @I>" ();
     (* core::ops::index::IndexMut<[T], I> *)

diff --git a/compiler/Logging.ml b/compiler/Logging.ml
@@ -27,6 +27,9 @@ let pure_micro_passes_log = L.get_logger "MainLogger.PureMicroPasses"
 (** Logger for ExtractBase *)
 let extract_log = L.get_logger "MainLogger.ExtractBase"
 
+(** Logger for ExtractBuiltin *)
+let builtin_log = L.get_logger "MainLogger.Builtin"
+
 (** Logger for Interpreter *)
 let interpreter_log = L.get_logger "MainLogger.Interpreter"
 

diff --git a/compiler/Main.ml b/compiler/Main.ml
@@ -38,6 +38,7 @@ let _ =
   symbolic_to_pure_log#set_level EL.Info;
   pure_micro_passes_log#set_level EL.Info;
   extract_log#set_level EL.Info;
+  builtin_log#set_level EL.Info;
   translate_log#set_level EL.Info;
   scc_log#set_level EL.Info;
   reorder_decls_log#set_level EL.Info