summaryrefslogtreecommitdiff
path: root/src/Translate.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Translate.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Translate.ml b/src/Translate.ml
index 2390dd69..13715865 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -64,6 +64,7 @@ let translate_function_to_symbolics (config : C.partial_config)
^ Print.fun_name_to_string fdef.A.name));
let { type_context; fun_context } = trans_ctx in
+ let fun_context = { C.fun_decls = fun_context.fun_decls } in
match fdef.body with
| None -> None
@@ -281,6 +282,8 @@ let translate_module_to_pure (config : C.partial_config)
(* Compute the type and function contexts *)
let type_context, fun_context = compute_type_fun_contexts m in
+ let fun_infos = FA.analyze_module m fun_context.C.fun_decls use_state in
+ let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in
let trans_ctx = { type_context; fun_context } in
(* Translate all the type definitions *)