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 |
|
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 |
|
Undocumented |
Variable |
|
Undocumented |
Variable | intersection |
Undocumented |
Variable | l |
Undocumented |
Variable |
|
Undocumented |
Variable |
|
Undocumented |
Variable |
|
Undocumented |
Variable |
|
Undocumented |
Variable |
|
Undocumented |
Variable |
|
Undocumented |
Variable |
|
Undocumented |
Variable | union |
Undocumented |
Variable | widen |
Undocumented |
Variable |
|
Undocumented |
Variable | _bvv |
Undocumented |
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.
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.
Undocumented
Undocumented
Undocumented
Value |
|
Undocumented
Value |
|
Undocumented
Value |
|
Undocumented
Value |
|
Undocumented
Value |
|
Undocumented
Value |
|
Undocumented
Value |
|
Undocumented
Value |
|