summaryrefslogtreecommitdiff
path: root/compiler/Translate.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Translate.ml6
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