mephi42
commented
4 years ago - mark certain inputs as symbolic
- use vex for propagation
- optimization: outputs for concrete inputs should be taken from trace
- record symbolic branch conditions
- concretize usages of symbolic addresses