You should see a fork if you divide by an unconstrained symbolic
value. One path is the divide by zero path, which triggers a CPU
exception. Note that S2E does not fully support floating point
operations, instead it emulates them with integer arithmetic. This
may add more constraints. Removing them may break execution
consistency and cause crashes elsewhere in the system.
What kind of analysis would you like to do? Perhaps there are
other ways that would not break execution consistency.
You received this message because you are a member of the S2E Developer Forum.
To post to this group, send email to s2e...@googlegroups.com
To unsubscribe from this group, send email to s2e-dev+u...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/s2e-dev
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/607b7a4a-9f03-43d6-be0a-cfe884302d8dn%40googlegroups.com.
The byte automatically becomes constrained after the division
operation is executed. If the byte wasn't constrained, it could
potentially be 0, which is impossible if execution were to proceed
past the division instruction. You would end up with a potentially
invalid test case.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/79cb5551-9ae8-4ccb-abcc-eaecf5466a28n%40googlegroups.com.
If the binary doesn't check the divisor, it should fork in the
helper_divx_XX functions in QEMU . You will have one path where
the program crashes with a division by zero exception and another
path where the program terminates normally. You can use S2E to
detect the crash and record the corresponding test case / path
constraints, and discard the other paths that don't crash. If the
binary does check the divisor, there won't be a fork in  and
the program will not crash.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/e12a5355-d68b-4a58-a871-a02ca92a6f07n%40googlegroups.com.