Just to be clear: we have a dynamic checker for integer problems. It adds paths to a program and then Klee tries to cover them.
The alternative approach of putting overflow checking into Klee is interesting and we haven't even looked into it. Also I meant to say that we're happy to share the patch. We'll put it on the web but in the meantime feel free to contact me separately. John On Sat, 26 Feb 2011, John Regehr wrote: > 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 > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
