Treat integer casts in a general manner

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 =