Module Dolmen_model.BitvSource

Value definition

************************************************************************

Sourcetype t = Z.t

Bitvectors, represented as unsigned, unbounded integers.

Sourceval ops : t Value.ops

ops for bitvector values.

Sourceval mk : int -> Z.t -> Value.t

mk n z Bitvector of size n, and bits z creation.

Sourceval builtins : Env.builtins

builtins for bitvectors

Sourceval ubitv : int -> Value.t -> Z.t

Extract the value as an unsigned integer

Sourceval sbitv : int -> Value.t -> Z.t

Extract the value as a signed integer