[klee-dev] klee crash question

[Daniel Dunbar]

Hey John,

On Dec 18, 2012, at 13: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?

It means that a buffer of Hagar size has symbolic data and will need
to be pushed to STP. Unfortunately, STP often has problems with large
arrays and may crash due to blowing the stack in some recursive
routines.

> Can I do anything about it?

Not too much. If you understand the zlib code well you can try to
rewrite it to use a smaller presumably temporary buffer. Or use the
argument Paul mentioned.

 - Daniel

> Blend
> Thanks,
>
> John Regehr
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev