Hi John, This issue seems to be similar to the one mentioned here http://keeda.stanford.edu/pipermail/klee-dev/2012-June/000873.html. A workaround is to give up some symbolic state by using --max-sym-array-size.
Some more information on the underlying problem is at http://keeda.stanford.edu/pipermail/klee-dev/2011-July/000698.html. Paul On 18 Dec 2012, at 21:55, John Regehr <reg...@cs.utah.edu> wrote: > Hi, > > I'm running Klee (checked out and compiled today) using LLVM 2.9 on 64-bit > Linux. I believe that I followed the build/install instructions exactly. > > My job here is to call the zlib function inflate() on a small (6-byte) > symbolic buffer. > > Klee runs for a while and generates 81 test cases but then dies like this: > > KLEE: WARNING ONCE: flushing 7152 bytes on read, may be slow and/or crash: > MO641[7152] allocated at zcalloc(): %2 = tail call noalias i8* @malloc(i64 > %1) nounwind, !dbg !5048 > > Does this mean anything that I can or should want to know? Can I do anything > about it? > > Thanks, > > John Regehr > > _______________________________________________ > 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
