On 15 December 2014 at 18:13, Dingbao Xie <[email protected]> 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 _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
