From 3151e373d64f9bce6146a44cd2d3cc64cac84cbf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 4 Sep 2023 00:59:39 +0200
Subject: Fix minor issues

---
 compiler/Driver.ml         |  4 +++-
 compiler/SymbolicToPure.ml | 14 ++++++++++++--
 2 files changed, 15 insertions(+), 3 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index b646a53d..d88962db 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -17,7 +17,9 @@ let log = main_log
 let _ =
   (* Set up the logging - for now we use default values - TODO: use the
    * command-line arguments *)
-  (* By setting a level for the main_logger_handler, we filter everything *)
+  (* By setting a level for the main_logger_handler, we filter everything.
+     To have a good trace: one should switch between Info and Debug.
+  *)
   Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
   main_log#set_level EL.Info;
   llbc_of_json_logger#set_level EL.Info;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 1a981de1..46eef953 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -242,6 +242,12 @@ let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
     ctx.trait_decls_ctx ctx.trait_impls_ctx generics.types
     generics.const_generics
 
+let ctx_egeneric_args_to_string (ctx : bs_ctx) (args : T.egeneric_args) : string
+    =
+  let fmt = bs_ctx_to_ctx_formatter ctx in
+  let fmt = Print.PC.ctx_to_etype_formatter fmt in
+  Print.PT.egeneric_args_to_string fmt args
+
 let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
   let fmt = Print.PC.ctx_to_rtype_formatter fmt in
@@ -381,8 +387,8 @@ let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
    of types: sty, forward types, backward types, etc.) *)
 let rec translate_generic_args (translate_ty : 'r T.ty -> ty)
     (generics : 'r T.generic_args) : generic_args =
-  (* Can't translate types with regions for now *)
-  assert (generics.regions = []);
+  (* We ignore the regions: if they didn't cause trouble for the symbolic execution,
+     then everything's fine *)
   let types = List.map translate_ty generics.types in
   let const_generics = generics.const_generics in
   let trait_refs =
@@ -1588,6 +1594,10 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
 
 and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     texpression =
+  log#ldebug
+    (lazy
+      ("translate_function_call:\n"
+      ^ ctx_egeneric_args_to_string ctx call.generics));
   (* Translate the function call *)
   let generics = ctx_translate_fwd_generic_args ctx call.generics in
   let args =
-- 
cgit v1.2.3