To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
val unk : 'a Value.sort -> 'a pure
unk s an unknown value of sort
This term explicitly denotes a term with undefined or unknown value.
val int : 's Bitv.t Value.sort -> word -> 's bitv
int s x is a bitvector constant
x of sort
div x y unsigned division modulo
2^'s truncating towards 0.
The division by zero is defined to be a vector of all ones of size
sdiv x y is signed division of
The signed division operator is defined in terms of the
div operator as follows:
/ | div x y : if not mx /\ not my | neg (div (neg x) y) if mx /\ not my x sdiv y = < | neg (div x (neg y)) if not mx /\ my | div (neg x) (neg y) if mx /\ my \ where mx = msb x, and my = msb y.
smodulo x y is the signed remainder of
div x y modulo
This version of the signed remainder where the sign follows the dividend, and is defined via the
% = modulo operation as follows
/ | x % y : if not mx /\ not my | neg (neg x % y) if mx /\ not my x smodulo y = < | neg (x % (neg y)) if not mx /\ my | neg (neg x % neg y) mod m if mx /\ my \ where mx = msb x and my = msb y.
shiftr s x m shifts
x right by
m bits filling with
shiftl s x m shifts
x left by
m bits filling with
val cast : 'a Bitv.t Value.sort -> bool -> 'b bitv -> 'a bitv
cast s b x casts
x to sort
s filling with
m = size s - size (sort b) > 0 then
b are prepended to the most significant part of the vector.
m <= 0, i.e., it is a narrowing cast, then the value of
b doesn't affect the result of evaluation.
val concat : 'a Bitv.t Value.sort -> 'b bitv list -> 'a bitv
concat s xs concatenates a list of vectors
All vectors are concatenated from left to right (so that the most significant bits of the resulting vector are defined by the first element of the list and so on).
The result of concatenation are then casted to sort
s with all extra bits (if any) set to
val append : 'a Bitv.t Value.sort -> 'b bitv -> 'c bitv -> 'a bitv
append s x y appends
y and casts to
y so that in the resulting vector the vector
x occupies the most significant part and
y the least significant part. The resulting vector is then casted to the sort
s with extra bits (if any) set to zero.
val perform : 'a Effect.sort -> 'a eff
perform s performs a generic effect of sort
repeat c data repeats data effects until the condition