diff options
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 9af3c71b..348183c5 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -3,6 +3,7 @@ open Types open Values open LlbcAst open Contexts +open Errors module SA = SymbolicAst module Micro = PureMicroPasses open TranslateCore @@ -126,6 +127,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) let ctx = { + meta = fdef.meta; decls_ctx = trans_ctx; SymbolicToPure.bid = None; sg; @@ -175,7 +177,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) SymbolicToPure.fresh_named_vars_for_symbolic_values input_svs ctx in { ctx with forward_inputs } - | _ -> raise (Failure "Unreachable") + | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable" in (* Add the backward inputs *) @@ -446,7 +448,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 - assert (trans.loops = []); + sanity_check __FILE__ __LINE__ (trans.loops = []) global.meta; let body = trans.f in let is_opaque = Option.is_none body.Pure.body in |