Module Region_bitvector

module Region_bitvector: sig .. end
Bitvectors with low-level regions

type 'a symbol 
module SubSymb: sig .. end
module SymbMap: Map.S  with type key = (int SymbMap.t) symbol
type t = [ `Symb of int SymbMap.t symbol
| `SymbSmt of Smt_bitvectors.smtBvExprAlt
| `Undef of int
| `Value of Dba.region * Bitvector.t ]
val region_equal : Dba.region -> Dba.region -> bool
val equal : t -> t -> bool

Construction functions


val create_constant : Bigint.t -> int -> t
create_constant v sz creates a bitvector of value bv with size sz in region `Constant
val zeros : int -> t
zeros size creates a bitvector of value 0 with size size in region `Constant
val undefined : int -> t
undefined n creates an undefined value of bitsize n
val pp : Format.formatter -> t -> unit
Pretty-printing

val to_string : t -> string
val region_of : t -> Dba.region

Accessors


val value_of : t -> Bigint.t
val bitvector_of : t -> Bitvector.t
val size_of : t -> int
val st_of : Bitvector.t -> string
val append : t -> t -> t
val non_deterministic : Dba.region -> int -> t
val restrict : t -> int -> int -> t
val succ : t -> t
include Sigs.Arithmetic
val lshift : t -> t -> t
val rshiftS : t -> t -> t
val rshiftU : t -> t -> t
val rotate_left : t -> t -> t
val rotate_right : t -> t -> t
val extension : t -> int -> t
val signed_extension : t -> int -> t
val eq : t -> t -> t
val diff : t -> t -> t
val leqU : t -> t -> t
val leqS : t -> t -> t
val ltU : t -> t -> t
val ltS : t -> t -> t
val gtU : t -> t -> t
val gtS : t -> t -> t
val geqU : t -> t -> t
val geqS : t -> t -> t
val lognot : t -> t
val logxor : t -> t -> t
val logor : t -> t -> t
val logand : t -> t -> t
val is_zero : t -> bool
val display_statistics : Format.formatter -> unit -> unit
val get_value : Smt_bitvectors.smtBvExprAlt ->
int ->
Smt_bitvectors.smtBvExprAlt list ->
Dba_types.Caddress.Set.t -> t
val get_expr : Smt_bitvectors.smtBvExprAlt ->
int ->
Smt_bitvectors.smtBvExprAlt list -> Dba_types.Caddress.Set.t -> Dba.expr
val get_byte_region_at : Bigint.t -> t
get_byte_region_at addr returns the value read at the lone byte cell addr.
val default_get_byte_region_at : Bigint.t -> t
default_get_byte_region_at addr is get_byte_region_at addr but catches the possible exception and returns an undefined byte instead.