diff options
| author | Nadrieril | 2024-05-06 15:42:48 +0200 |
|---|---|---|
| committer | Nadrieril | 2024-05-06 15:50:27 +0200 |
| commit | 87da55498b0ba19c74854f3e8218fab857c624e3 (patch) | |
| tree | 2101e01f490e9f9821d7b0105bab2568a4d572c9 /compiler/InterpreterExpressions.ml | |
| parent | a935064196f7fcc65355726a523508f4317d16ee (diff) | |
Update charon
Diffstat (limited to 'compiler/InterpreterExpressions.ml')
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 5f849230..5a4fe7da 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -551,7 +551,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) | Ge -> Z.geq sv1.value sv2.value | Gt -> Z.gt sv1.value sv2.value | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr | Shl - | Shr | Ne | Eq -> + | Shr | Ne | Eq | CheckedAdd | CheckedSub | CheckedMul -> craise __FILE__ __LINE__ meta "Unreachable" in Ok @@ -575,7 +575,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) | BitXor -> raise Unimplemented | BitAnd -> raise Unimplemented | BitOr -> raise Unimplemented - | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq -> + | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq | CheckedAdd + | CheckedSub | CheckedMul -> craise __FILE__ __LINE__ meta "Unreachable" in match res with @@ -586,7 +587,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) value = VLiteral (VScalar sv); ty = TLiteral (TInteger sv1.int_ty); }) - | Shl | Shr -> raise Unimplemented + | Shl | Shr | CheckedAdd | CheckedSub | CheckedMul -> + craise __FILE__ __LINE__ meta "Unimplemented binary operation" | Ne | Eq -> craise __FILE__ __LINE__ meta "Unreachable") | _ -> craise __FILE__ __LINE__ meta "Invalid inputs for binop" @@ -633,6 +635,10 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop) | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta; TLiteral (TInteger int_ty1) + (* These return `(int, bool)` which isn't a literal type *) + | CheckedAdd | CheckedSub | CheckedMul -> + craise __FILE__ __LINE__ meta + "Checked operations are not implemented" | Shl | Shr -> (* The number of bits can be of a different integer type than the operand *) |