[klee-dev] KLEE on integer overflow?

[Luca Dariz]

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