diff options
Diffstat (limited to '')
-rw-r--r-- | src/InterpreterExpressions.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index e46ca721..4549365d 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -274,6 +274,15 @@ let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand) match mk_scalar sv.int_ty i with | Error _ -> cf (Error EPanic) | Ok sv -> cf (Ok { v with V.value = V.Concrete (V.Scalar sv) })) + | E.Cast (src_ty, tgt_ty), V.Concrete (V.Scalar sv) -> ( + assert (src_ty == sv.int_ty); + let i = sv.V.value in + match mk_scalar tgt_ty i with + | Error _ -> cf (Error EPanic) + | Ok sv -> + let ty = T.Integer tgt_ty in + let value = V.Concrete (V.Scalar sv) in + cf (Ok { V.ty; value })) | _ -> raise (Failure "Invalid input for unop") in comp eval_op apply cf @@ -291,6 +300,7 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand) match (unop, v.V.ty) with | E.Not, T.Bool -> T.Bool | E.Neg, T.Integer int_ty -> T.Integer int_ty + | E.Cast (_, tgt_ty), _ -> T.Integer tgt_ty | _ -> raise (Failure "Invalid input for unop") in let res_sv = |