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.
Last modified 1yr ago
Copy link