Il 13/10/2014 23:47, Mark R. Tuttle ha scritto:
*Can KLEE check for integer overflow?*
Since KLEE is based on STP and STP is based on a theory of bit vectors,
I had hoped it might be easy for KLEE to check for an overflow bit.Since
CLANG has -fsanitize=unsigned-integer-overflow and -fsanitize=integer I
had hoped it would be easy to compile with these flags and run KLEE, but
KLEE does not appear to support the LLVM arithmetic with overflow
intrinsics like llvm.uadd.with.overflow.* that CLANG inserts.
Hi Mark,
the implementation of these intrinsics is just incomplete, I started to
expand it to detect unsigned integer overflow in this branch
https://github.com/luckyluke/klee/tree/detect-overflow.
Best Regards,
Luca Dariz
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
