[klee-dev] klee crash question

[Paul Marinescu]

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 <regehr at 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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed