Mark R. Tuttle
2014-10-13 21:47:22 UTC
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.
*Is there a list of all the things that KLEE can be made to check for*?
Things like bad pointers and division by zero, while generating inputs to
*What is the most effective way to become more deeply plugged into the KLEE
Is there a workshop or publication venue where people tend to
do people go to brainstorm about potential applications and solutions? This
list is the only resource Iâm aware of.
Mark Tuttle, email@example.com