Hi, I believe the answer is yes and we have been using KLEE for verification for years. It indeed catches all the out-of-bound errors and that is one of the several common issues we catch.
Thanks Gao On Tue, Nov 13, 2018 at 7:37 AM Kornilios Kourtis <kornil...@gmail.com> wrote: > Hi, > > I've been playing around with klee, and so far it seems like a great tool! > > One thing I'm wondering is whether it can be used for verification > (I'm thinking small pieces of code here). For example, in principle > (ignoring potential klee code bugs) will klee _always_ report errors > on code with out-of-bounds accesses? From a quick look at the code, > the answer seems to be "yes", because whenever klee compromises it > reports an error or warning. On the other hand, I have not seen such a > use-case mentioned, so maybe I'm missing something. > > Thanks, > Kornilios. > > -- > Kornilios Kourtis > > _______________________________________________ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev