summaryrefslogtreecommitdiff
path: root/src/SymbolicToPure.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/SymbolicToPure.ml6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 3ac68365..42479a6e 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1177,6 +1177,12 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression)
in
(ctx, Unop (Neg int_ty), effect_info, args, None)
| _ -> raise (Failure "Unreachable"))
+ | S.Unop (E.Cast (src_ty, tgt_ty)) ->
+ (* Note that cast can fail *)
+ let effect_info =
+ { can_fail = true; input_state = false; output_state = false }
+ in
+ (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, None)
| S.Binop binop -> (
match args with
| [ arg0; arg1 ] ->