summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAymeric Fromherz2023-09-22 16:48:37 +0200
committerAymeric Fromherz2023-09-22 16:48:37 +0200
commita5f87ba02342ae0b96fe0d8ba16f1ec78469d760 (patch)
tree2c62e9cc27a453aaeec753760a63d715e76b545d
parente75879992c5a5a5102a4c5f20b90e6a1032b8ec5 (diff)
Allow bitshifts with any pair of integer types
Diffstat (limited to '')
-rw-r--r--compiler/SymbolicToPure.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 3512270a..08f67592 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1542,7 +1542,11 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
| [ arg0; arg1 ] ->
let int_ty0 = ty_as_integer arg0.ty in
let int_ty1 = ty_as_integer arg1.ty in
- assert (int_ty0 = int_ty1);
+ (match binop with
+ (* The Rust compiler accepts bitshifts for any integer type combination for ty0, ty1 *)
+ | E.Shl | E.Shr -> ()
+ | _ -> assert (int_ty0 = int_ty1)
+ );
let effect_info =
{
can_fail = ExpressionsUtils.binop_can_fail binop;