a load operation is based on a register containing a symbolic variable (potential arbitrary read)
a store operation is based on a register containing a symbolic variable (potential arbitrary write)
To do so, it is checked whether the involved (symbolic) register may take on a different concrete value than it currently does. In addition to this check, it should also be validated that the path constraints are still satisfiable.
The same thematic applies to the control hijacker analysis.
Testing
[x] Implement fixes
[x] Check that tests/control_flow still work
[x] Check that tests/hijack_indirect_callsite still work
Description
The memory hijacker analysis checks if
To do so, it is checked whether the involved (symbolic) register may take on a different concrete value than it currently does. In addition to this check, it should also be validated that the path constraints are still satisfiable.
The same thematic applies to the control hijacker analysis.
Testing
tests/control_flowstill worktests/hijack_indirect_callsitestill work