diff --git a/src/lib/partial_eval.ml b/src/lib/partial_eval.ml index c19d1190a..e8e9fc0a3 100644 --- a/src/lib/partial_eval.ml +++ b/src/lib/partial_eval.ml @@ -347,8 +347,8 @@ module AbsValue : SAIL_VALUE = struct ("abs_int", lift Z.abs (Int @-> Ret Int)); ("div_int", lift Z.div (Int @-> Int @-> Ret Int)); ("tdiv_int", lift Z.div (Int @-> Int @-> Ret Int)); - ("quotient", lift Z.div (Int @-> Int @-> Ret Int)); - ("modulus", lift Z.rem (Int @-> Int @-> Ret Int)); + ("quotient", lift Z.ediv (Int @-> Int @-> Ret Int)); + ("modulus", lift Z.erem (Int @-> Int @-> Ret Int)); ("tmod_int", lift Z.rem (Int @-> Int @-> Ret Int)); ("eq_int", lift Z.equal (Int @-> Int @-> Ret Bool)); ("quot_round_zero", lift Z.div (Int @-> Int @-> Ret Int)); @@ -397,6 +397,8 @@ module AbsValue : SAIL_VALUE = struct ("uint", lift TransferBitvectorInterval.Ops.unsigned (AbsBV @-> Ret AbsInt)); ("sint", lift TransferBitvectorInterval.Ops.signed (AbsBV @-> Ret AbsInt)); ("pow2", lift Sail_lib.pow2 (Int @-> Ret Int)); + ("shl_int", lift (fun i n -> Sail_lib.shl_int (i, n)) (Int @-> Int @-> Ret Int)); + ("shr_int", lift (fun i n -> Sail_lib.shr_int (i, n)) (Int @-> Int @-> Ret Int)); ("concat_str", lift ( ^ ) (String @-> String @-> Ret String)); ("string_of_bits", lift Sail_lib.string_of_bits (BV @-> Ret String)); ("eq_string", lift ( = ) (String @-> String @-> Ret Bool));