diff options
author | Guillaume Boisseau | 2024-04-18 14:14:53 +0200 |
---|---|---|
committer | GitHub | 2024-04-18 14:14:53 +0200 |
commit | 8cd6090128397dd9dccf5bb7c27dd85f318aa3c5 (patch) | |
tree | d2f2bd4b415f55ff4830e35c4883727b89136577 /compiler/Translate.ml | |
parent | b4c3829305cac70827f6cbca2e90b0ef8be00d47 (diff) | |
parent | 6ef342ea6ceb0a49929859ef96c5e0afcea7451f (diff) |
Merge pull request #116 from AeneasVerif/item_meta
Diffstat (limited to '')
-rw-r--r-- | compiler/Translate.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 9460c5f4..222b3c57 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -127,7 +127,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx) let ctx = { - meta = fdef.meta; + meta = fdef.item_meta.meta; decls_ctx = trans_ctx; SymbolicToPure.bid = None; sg; @@ -179,7 +179,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx) SymbolicToPure.fresh_named_vars_for_symbolic_values input_svs ctx in { ctx with forward_inputs } - | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable" + | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable" in (* Add the backward inputs *) @@ -486,7 +486,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) let global_decls = ctx.trans_ctx.global_ctx.global_decls in let global = GlobalDeclId.Map.find id global_decls in let trans = FunDeclId.Map.find global.body ctx.trans_funs in - sanity_check __FILE__ __LINE__ (trans.loops = []) global.meta; + sanity_check __FILE__ __LINE__ (trans.loops = []) global.item_meta.meta; let body = trans.f in let is_opaque = Option.is_none body.Pure.body in |