Negate, Inject & Restore
In the next example we are using the snapshot engine:
- Passing a file as argument.
- We select we want to use the symbolic engine.
- We taint the buffer that
fread()reads from the file.
- We create a snapshot in the function that parses the buffer read from the file.
- When a condition is evaluated we negate it, inject the solution in memory and restore the snapshot with it.
- The solution will be "valid" so we will satisfy the existent conditions.