diff options
author | Aymeric Fromherz | 2023-09-22 16:48:37 +0200 |
---|---|---|
committer | Aymeric Fromherz | 2023-09-22 16:48:37 +0200 |
commit | a5f87ba02342ae0b96fe0d8ba16f1ec78469d760 (patch) | |
tree | 2c62e9cc27a453aaeec753760a63d715e76b545d | |
parent | e75879992c5a5a5102a4c5f20b90e6a1032b8ec5 (diff) |
Allow bitshifts with any pair of integer types
Diffstat (limited to '')
-rw-r--r-- | compiler/SymbolicToPure.ml | 6 |
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; |