add | Unsigned addition | BitVec | BitVec |
signed_add | Signed addition | BitVec | BitVec |
sub | Unsigned subtraction | BitVec | BitVec |
signed_sub | Signed subtraction | BitVec | BitVec |
mul | Unsigned multiplication | BitVec | BitVec |
signed_mul | Signed multiplication | BitVec | BitVec |
div | Unsigned division | BitVec | BitVec |
signed_div | Signed division | BitVec | BitVec |
mod | Unsigned modulo | BitVec | BitVec |
signed_mod | Signed modulo | BitVec | BitVec |
carry | Returns 1 if unsigned addition would carry, 0 otherwise | BitVec | BitVec |
signed_carry | Returns 1 if signed addition would carry, 0 otherwise | BitVec | BitVec |
signed_borrow | Returns 1 if signed subtraction would borrow, 0 otherwise | BitVec | BitVec |
signed | Marks the BitVec as signed | — | BitVec |
unsigned | Marks the BitVec as unsigned | — | BitVec |
cast | Casts the BitVec to a different bit size | number | BitVec |
unsigned_cast | Casts the BitVec to a different bit size as unsigned | number | BitVec |
signed_cast | Casts the BitVec to a different bit size as signed (sign-extends) | number | BitVec |
is_one | Returns true if the value is 1 | — | boolean |
is_zero | Returns true if the value is 0 | — | boolean |
msb | Returns the most significant bit | — | number |
lsb | Returns the least significant bit | — | number |
is_signed | Returns true if marked as signed | — | boolean |
is_unsigned | Returns true if marked as unsigned | — | boolean |
bits | Returns the number of bits | — | number |
abs | Returns the absolute value | — | BitVec |
neg | Returns the negation | — | BitVec |
bnot | Bitwise NOT | — | BitVec |
band | Bitwise AND | BitVec | BitVec |
bor | Bitwise OR | BitVec | BitVec |
bxor | Bitwise XOR | BitVec | BitVec |
shl | Shift left | BitVec | BitVec |
shr | Shift right | BitVec | BitVec |
signed_shr | Shift right (sign-extending) | BitVec | BitVec |
count_ones | Returns the number of 1 bits | — | number |
count_zeros | Returns the number of 0 bits | — | number |
leading_ones | Returns the number of leading 1 bits | — | number |
leading_zeros | Returns the number of leading 0 bits | — | number |
succ | Returns the successor (adds 1) | — | BitVec |
incr_by | Increments by specified amount | number | BitVec |
pred | Returns the predecessor (subtracts 1) | — | BitVec |
decr_by | Decrements by specified amount | number | BitVec |
extract | Extracts bits from lsb offset to msb offset (exclusive) | (number, number) | BitVec |
concat | Concatenates two bit-vectors | BitVec | BitVec |
is_exactly_equal | Returns true if both value and bit size are equal | BitVec | boolean |
to_address | Converts to an AddressValue | — | AddressValue |
to_u64 | Converts to unsigned 64-bit integer | — | number |
to_i64 | Converts to signed 64-bit integer | — | number |
to_u32 | Converts to unsigned 32-bit integer | — | number |
to_i32 | Converts to signed 32-bit integer | — | number |
to_be_bytes | Converts to big-endian byte array | — | number[] |
to_le_bytes | Converts to little-endian byte array | — | number[] |
to_bytes | Converts to native-endian byte array | — | number[] |
to_string | Converts to string representation | — | string |
to_hex_string | Converts to hexadecimal string representation | — | string |
to_binary_string | Converts to binary string representation | — | string |