summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/InterpreterStatements.ml6
-rw-r--r--src/Translate.ml6
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