module documentation

Undocumented

Class BV A class representing an AST of operations culminating in a bitvector. Do not instantiate this class directly, instead use BVS or BVV to construct a symbol or value, and then use operations to construct more complicated expressions.
Function BVS Creates a bit-vector symbol (i.e., a variable).
Function BVV Creates a bit-vector value (i.e., a concrete value).
Function cleanup Undocumented
Function DSIS Undocumented
Function ESI Undocumented
Function SI Undocumented
Function TSI Undocumented
Function ValueSet Undocumented
Constant SGE Undocumented
Constant SGT Undocumented
Constant SLE Undocumented
Constant SLT Undocumented
Constant UGE Undocumented
Constant UGT Undocumented
Constant ULE Undocumented
Constant ULT Undocumented
Variable Concat Undocumented
Variable Extract Undocumented
Variable intersection Undocumented
Variable l Undocumented
Variable LShR Undocumented
Variable Reverse Undocumented
Variable RotateLeft Undocumented
Variable RotateRight Undocumented
Variable SDiv Undocumented
Variable SignExt Undocumented
Variable SMod Undocumented
Variable union Undocumented
Variable widen Undocumented
Variable ZeroExt Undocumented
Variable _bvv_cache Undocumented
def BVS(name, size, min=None, max=None, stride=None, uninitialized=False, explicit_name=None, discrete_set=False, discrete_set_max_card=None, **kwargs): (source)

Creates a bit-vector symbol (i.e., a variable). If you want to specify the maximum or minimum value of a normal symbol that is not part of value-set analysis, you should manually add constraints to that effect. **Do not use ``min`` and ``max`` for symbolic execution.** :param name: The name of the symbol. :param size: The size (in bits) of the bit-vector. :param min: The minimum value of the symbol, used only for value-set analysis :param max: The maximum value of the symbol, used only for value-set analysis :param stride: The stride of the symbol, used only for value-set analysis :param uninitialized: Whether this value should be counted as an "uninitialized" value in the course of an analysis. :param bool explicit_name: If False, an identifier is appended to the name to ensure uniqueness. :param bool discrete_set: If True, a DiscreteStridedIntervalSet will be used instead of a normal StridedInterval. :param int discrete_set_max_card: The maximum cardinality of the discrete set. It is ignored if discrete_set is set to False or None. :returns: a BV object representing this symbol.

def BVV(value, size=None, **kwargs): (source)

Creates a bit-vector value (i.e., a concrete value). :param value: The value. Either an integer or a bytestring. If it's the latter, it will be interpreted as the bytes of a big-endian constant. :param size: The size (in bits) of the bit-vector. Optional if you provide a string, required for an integer. :returns: A BV object representing this value.

def cleanup(): (source)

Undocumented

def DSIS(name=None, bits=0, lower_bound=None, upper_bound=None, stride=None, explicit_name=None, to_conv=None, max_card=None): (source)

Undocumented

def ESI(bits, **kwargs): (source)

Undocumented

def SI(name=None, bits=0, lower_bound=None, upper_bound=None, stride=None, to_conv=None, explicit_name=None, discrete_set=False, discrete_set_max_card=None): (source)

Undocumented

def TSI(bits, name=None, uninitialized=False, explicit_name=None): (source)

Undocumented

def ValueSet(bits, region=None, region_base_addr=None, value=None, name=None, val=None): (source)

Undocumented

Undocumented

Value
operations.op('SGE', (BV, BV), Bool,
              extra_check=operations.length_same_check, bound=False)

Undocumented

Value
operations.op('SGT', (BV, BV), Bool,
              extra_check=operations.length_same_check, bound=False)

Undocumented

Value
operations.op('SLE', (BV, BV), Bool,
              extra_check=operations.length_same_check, bound=False)

Undocumented

Value
operations.op('SLT', (BV, BV), Bool,
              extra_check=operations.length_same_check, bound=False)

Undocumented

Value
operations.op('__ge__', (BV, BV), Bool,
              extra_check=operations.length_same_check, bound=False)

Undocumented

Value
operations.op('__gt__', (BV, BV), Bool,
              extra_check=operations.length_same_check, bound=False)

Undocumented

Value
operations.op('__le__', (BV, BV), Bool,
              extra_check=operations.length_same_check, bound=False)

Undocumented

Value
operations.op('__lt__', (BV, BV), Bool,
              extra_check=operations.length_same_check, bound=False)

Undocumented

Undocumented

intersection = (source)

Undocumented

Undocumented

Undocumented

Undocumented

RotateLeft = (source)

Undocumented

RotateRight = (source)

Undocumented

Undocumented

Undocumented

Undocumented

Undocumented

Undocumented

Undocumented

_bvv_cache: dict = (source)

Undocumented