[klee-dev] KLEE on integer overflow?

[Mark R. Tuttle]

*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.


*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
induce coverage?


*What is the most effective way to become more deeply plugged into the KLEE
community?*

Is there a workshop or publication venue where people tend to
congregate?  Where
do people go to brainstorm about potential applications and solutions?  This
list is the only resource I’m aware of.


Thanks,
Mark


Mark Tuttle, tuttle at acm.org
-------------- next part --------------
HTML attachment scrubbed and removed