Module F.Bv

type t
val const : int -> string -> t

const size name creates the (first-order) constant of size bits named name .

val value : int -> Z.t -> t

value sz bv creates a constant from the bitvector value bv of size sz.

include Binsec.Sigs.COMPARISON with type t := t and type boolean := Bl.t
val equal : t -> t -> Bl.t
val diff : t -> t -> Bl.t
val ule : t -> t -> Bl.t
val uge : t -> t -> Bl.t
val ult : t -> t -> Bl.t
val ugt : t -> t -> Bl.t
val sle : t -> t -> Bl.t
val sge : t -> t -> Bl.t
val slt : t -> t -> Bl.t
val sgt : t -> t -> Bl.t
include Binsec.Sigs.ARITHMETIC with type t := t
val add : t -> t -> t
val sub : t -> t -> t
val mul : t -> t -> t
val neg : t -> t
val udiv : t -> t -> t
val umod : t -> t -> t
val urem : t -> t -> t
val sdiv : t -> t -> t
val smod : t -> t -> t
val srem : t -> t -> t
include Binsec.Sigs.EXTENDED_LOGICAL with type t := t
include Binsec.Sigs.LOGICAL with type t := t
val logand : t -> t -> t
val logor : t -> t -> t
val lognot : t -> t
val logxor : t -> t -> t
val lognand : t -> t -> t

lognand x y creates the nand bitvector operation between x and y.

val lognor : t -> t -> t

lognor x y creates the nor bitvector operation between x and y.

val logxnor : t -> t -> t

logxnor x y creates the xnor bitvector operation between x and y.

include Binsec.Sigs.SHIFT_ROT with type t := t and type index := t
val shift_left : t -> t -> t
val shift_right : t -> t -> t
val shift_right_signed : t -> t -> t
val rotate_left : t -> t -> t
val rotate_right : t -> t -> t
val rotate_lefti : t -> int -> t

rotate_lefti x i same as rotate_left but with a constant index.

val rotate_righti : t -> int -> t

rotate_righti x i same as rotate_right but with a constant index.

val append : t -> t -> t

append x y creates the concatenation of the two bitvectors x and y.

val extract : hi:int -> lo:int -> t -> t

extract ~hi ~lo x extracts the sub-bitvector of x starting from bit lo and ending at bit hi (included).

val uext : int -> t -> t

uext n x zero-extends the bitvector x by adding n bits.

val sext : int -> t -> t

sext n x sign extends the bitvector x copying n times the most significant bit.

val ite : Bl.t -> t -> t -> t

ite x y z creates the bitvector ite operation between y and z according to x.

val succ : t -> t

succ x creates the bitvector x + 1 operation.

val to_bl : t -> Bl.t

to_bl x cast the 1-bit bitvector x as a boolean.