summaryrefslogtreecommitdiff
path: root/compiler/SymbolicToPure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/SymbolicToPure.ml')
-rw-r--r--compiler/SymbolicToPure.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 0c30f44c..1701891f 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1963,6 +1963,9 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx)
(* Return the computed information *)
!info
+let translate_meta (meta : Meta.meta option) (msg : string) : texpression =
+ { e = EError (meta, msg); ty = Error }
+
let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
match e with
| S.Return (ectx, opt_v) ->
@@ -1989,6 +1992,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
*)
translate_forward_end ectx loop_input_values e back_e ctx
| Loop loop -> translate_loop loop ctx
+ | Error (meta, msg) -> translate_meta meta msg
and translate_panic (ctx : bs_ctx) : texpression =
(* Here we use the function return type - note that it is ok because