[klee-dev] Bug in overflow error reporting and a quick question

[Martin Hořeňovský]

Hello,

currently KLEE reports both signed and unsigned overflows as "overflow
on unsigned <op>" which is obviously wrong. Quick look through commits
adding overflow checking says that this is caused by ie all
subtraction overflows being handled by
"SpecialFunctionHandler::handleSubOverflow" which has hardcoded string
"overflow on unsigned subtraction". This should be fairly easy to fix
and I intend to do it, hopefully right after this weekend.


Also I have a question, how difficult, or rather how substantial,
performance improving commits have to be to be accepted? Because even
while quickly browsing KLEE code I found places that were
unnecessarily pessimized, by things like not calling .reserve() on a
vector before filling it with known number of items and I was
wondering whether if I started collecting and fixing them, I should
commit the changes back.

Best Regards
Martin Hořeňovský