diff options
Diffstat (limited to '')
-rw-r--r-- | compiler/LlbcAstUtils.ml | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 8c8bbabe..a982af30 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -15,13 +15,22 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : (** Return the opaque declarations found in the crate. + [filter_assumed]: if [true], do not consider as opaque the external definitions + that we will map to definitions from the standard library. + Remark: the list of functions also contains the list of opaque global bodies. *) -let crate_get_opaque_decls (k : crate) : T.type_decl list * fun_decl list = +let crate_get_opaque_decls (k : crate) (filter_assumed : bool) : + T.type_decl list * fun_decl list = let open ExtractAssumed in let is_opaque_fun (d : fun_decl) : bool = let sname = name_to_simple_name d.name in - d.body = None && not (SimpleNameMap.mem sname assumed_globals_map) + d.body = None + (* Something to pay attention to: we must ignore trait method *declarations* + (which don't have a body but must not be considered as opaque) *) + && (match d.kind with TraitMethodDecl _ -> false | _ -> true) + && ((not filter_assumed) + || not (SimpleNameMap.mem sname assumed_globals_map)) in let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in (* Note that by checking the function bodies we also the globals *) @@ -30,5 +39,5 @@ let crate_get_opaque_decls (k : crate) : T.type_decl list * fun_decl list = (** Return true if the crate contains opaque declarations, ignoring the assumed definitions. *) -let crate_has_opaque_decls (k : crate) : bool = - crate_get_opaque_decls k <> ([], []) +let crate_has_opaque_decls (k : crate) (filter_assumed : bool) : bool = + crate_get_opaque_decls k filter_assumed <> ([], []) |