Description

The MODE namespace contains all kinds of modes.

Example

>>> setMode(MODE.ONLY_ON_TAINTED, True)

MODE.ALIGNED_MEMORY
Keeps a map of aligned memory to reduce the symbolic memory explosion of LOAD and STORE accesses.
MODE.AST_OPTIMIZATIONS
Reduces the depth of the trees using classical arithmetic optimisations.
MODE.CONCRETIZE_UNDEFINED_REGISTERS
Concretizes every register tagged as undefined (see #750).
MODE.CONSTANT_FOLDING
Performs a constant folding optimization of sub ASTs which do not contain symbolic variables.
MODE.MEMORY_ARRAY
Enables symbolic pointers reasoning (QF_ABV logic). When this mode is not enabled, which is the case by default, the QF_BV memory model is applied.
MODE.ONLY_ON_SYMBOLIZED
Removes symbolic expressions that does not contain symbolic variable.
MODE.ONLY_ON_TAINTED
Removes symbolic expressions that are not tainted.
MODE.PC_TRACKING_SYMBOLIC
Tracks path constraints only if they are symbolized. This mode is enabled by default.
MODE.SYMBOLIZE_INDEX_ROTATION
Symbolizes the index of rotation for bvror and bvrol nodes. This mode increases the complexity of solving.
MODE.SYMBOLIZE_LOAD
Keeps symbolic expressions on load indexes (concretize them otherwise).
MODE.SYMBOLIZE_STORE
Keeps symbolic expressions on store indexes (concretize them otherwise).
MODE.TAINT_THROUGH_POINTERS
Spreads taint in non MEMORY_ARRAY mode if an index pointer is tainted (see #725).