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

Cristian Cadar c.cadar at imperial.ac.uk
Sat Mar 7 12:56:48 GMT 2015


On 04/03/2015 22:55, Martin Hořeňovský wrote:
> 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.
Great, please submit a pull request.

> 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.
Given KLEE's algorithmic complexity, some performance optimisations are
simply not worth it, especially if they make the code harder to
understand.  But we can discuss specific proposals on GitHub.

Best,
Cristian

> 
> Best Regards
> Martin Hořeňovský
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> 



More information about the klee-dev mailing list