[klee-dev] APint::udiv assertion fails

[Dan Liew]

On 15 December 2014 at 18:13, Dingbao Xie <xiedingbao at gmail.com> wrote:
> Hi, everyone
> I encountered an assertion failure when trying to test grep with klee.
> The complete stack trace is shown below:
>

Looks like a division by zero happened whilst evaluating an
instruction that uses constants. KLEE's division by zero check [1]
(implemented as an instrumentation pass) should prevent that from
happening but obviously it did not in this case. You need to take a
look at the LLVM IR around the instruction to check if the division by
zero instrumentation was inserted properly before the (presumably)
sdiv instruction.

- If the instrumentation is present you need to work out why it didn't
detect the division by zero
- If the instrumentation is missing you need to work out why its missing.


[1] https://github.com/klee/klee/blob/master/lib/Module/Checks.cpp#L54