ccadar/klee — pull request #64 by delcypher (2013-11-07 16:17:38+00:00)
Title: Overshift fixes

This makes LLVM and STPBuilder's notion of overshifting for the Shr, AShr and LShr operators the same by changing STPBuilder's behaviour to always overshift to zero.

I've added a several tests to check this (which all fail on current KLEE).

These changes could have a lot of impact if I get them wrong so I'd like someone else to look over these changes. They don't break anything in the test-suite but of course that's not much of a guarantee...

@hpalikareva : I didn't touch the MetaSMTBuilder so you might want to check that when using the MetaSMTBuilder you can pass all the tests I add here. Notice once I fixed all the operators the getShiftBits() function wasn't needed any more in the STPBuilder :)