One of my students has a Clang patch that implements comprehensive integer undefined behavior checking (it doesn't check for unsigned overflow, since those are well-defined, but it would be easy to modify to check for those).
The inserted checks are Klee-compatible (in contrast with the checks inserted by Clang's -ftrapv, which I believe uses overflow intrinsics that Klee doesn't currently understand). John
