diff options
author | Son Ho | 2023-10-25 15:36:06 +0200 |
---|---|---|
committer | Son Ho | 2023-10-25 15:36:06 +0200 |
commit | e3cb3646bbe3d50240aa0bf4763f8e816fb9a706 (patch) | |
tree | f6b58bcd7ce1f9becba0b292adfc087a9e099135 /compiler/Translate.ml | |
parent | a41299c8543fe12f98ae2554bc9cefca6990af5f (diff) |
Fix some issues at extraction and add builtins
Diffstat (limited to 'compiler/Translate.ml')
-rw-r--r-- | compiler/Translate.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 35dff9e6..019a5c35 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -390,10 +390,10 @@ type gen_config = { [filter_assumed]: if [true], do not consider as opaque the external definitions that we will map to definitions from the standard library. *) -let crate_has_opaque_decls (ctx : gen_ctx) (filter_assumed : bool) : bool * bool - = +let crate_has_opaque_non_builtin_decls (ctx : gen_ctx) (filter_assumed : bool) : + bool * bool = let types, funs = - LlbcAstUtils.crate_get_opaque_decls ctx.crate filter_assumed + LlbcAstUtils.crate_get_opaque_non_builtin_decls ctx.crate filter_assumed in log#ldebug (lazy @@ -1257,7 +1257,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (* Check if there are opaque types and functions - in which case we need * to split *) - let has_opaque_types, has_opaque_funs = crate_has_opaque_decls ctx true in + let has_opaque_types, has_opaque_funs = + crate_has_opaque_non_builtin_decls ctx true + in let has_opaque_types = has_opaque_types || !Config.use_state in (* Extract the types *) |