diff options
author | Son Ho | 2023-11-13 13:27:02 +0100 |
---|---|---|
committer | Son Ho | 2023-11-13 13:27:02 +0100 |
commit | 6c88d30031255c0ac612b67bb5b3c20c2f07e563 (patch) | |
tree | 8b0c28f8eb8bb6e76604b7e66eb84b0940d59f03 /compiler/Translate.ml | |
parent | 746239e8f29de85f848d14e44eac8690e2065a1d (diff) |
Add RegionsHierarchy.ml
Diffstat (limited to '')
-rw-r--r-- | compiler/Translate.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 9a6addee..2aedb544 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -91,6 +91,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) SymbolicToPure.llbc_fun_decls = trans_ctx.fun_ctx.fun_decls; fun_sigs; fun_infos = trans_ctx.fun_ctx.fun_infos; + regions_hierarchies = trans_ctx.fun_ctx.regions_hierarchies; } in let global_context = @@ -263,9 +264,11 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* Translate *) SymbolicToPure.translate_fun_decl ctx (Some symbolic) in - let pure_backwards = - List.map translate_backward fdef.signature.regions_hierarchy + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find (FRegular fdef.def_id) + fun_context.regions_hierarchies in + let pure_backwards = List.map translate_backward regions_hierarchy in (* Return *) (pure_forward, pure_backwards) |