From 85956db556c182f72e53ffcb91d32dd2e21d81f1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Mar 2022 23:26:03 +0100
Subject: Fix minor issues

---
 src/InterpreterStatements.ml | 6 +++++-
 src/Translate.ml             | 6 +++---
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index ef7c09e8..5a700f1a 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -1009,7 +1009,11 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
   (* We can evaluate the function call only if it is not opaque *)
   let body =
     match def.body with
-    | None -> raise (Failure "Can't evaluate a call to an opaque function")
+    | None ->
+        raise
+          (Failure
+             ("Can't evaluate a call to an opaque function: "
+             ^ Print.name_to_string def.name))
     | Some body -> body
   in
   let tsubst =
diff --git a/src/Translate.ml b/src/Translate.ml
index e547ad60..d337f5b8 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -602,7 +602,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   (* First compute the filename by replacing the extension and converting the
    * case (rust module names are snake case) *)
   let module_name, extract_filebasename =
-    match Filename.chop_suffix_opt ~suffix:".llbc" filename with
+    match Filename.chop_suffix_opt ~suffix:".cfim" filename with
     | None ->
         (* Note that we already checked the suffix upon opening the file *)
         failwith "Unreachable"
@@ -660,7 +660,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
 
     (* Extract the types *)
     (* If there are opaque types, we extract in an interface *)
-    let types_filename_ext = if has_opaque_types then ".fst" else ".fsti" in
+    let types_filename_ext = if has_opaque_types then ".fsti" else ".fst" in
     let types_filename = extract_filebasename ^ ".Types" ^ types_filename_ext in
     let types_module = module_name ^ ".Types" in
     let types_config =
@@ -703,7 +703,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
           }
         in
         extract_file opaque_config gen_ctx opaque_filename m.M.name
-          opaque_module ": type definitions" [] [];
+          opaque_module ": opaque function definitions" [] [ types_module ];
         [ opaque_module ])
       else []
     in
-- 
cgit v1.2.3