[klee-dev] reproducing the bugs found by KLEE

[Daniel Dunbar]

On Mon, Oct 19, 2009 at 2:16 PM, Cristian Zamfir
<cristian.zamfir at epfl.ch> wrote:
>
> Hi,
>
> I am trying to reproduce the bugs from the OSDI paper.
>
> I managed to reproduce 7 bugs on the native binaries: using the
> instructions in the paper, it worked for paste, mkdir, mknod, mkfifo,
> tac, seq and "ptx -F\\ abcdefghijklmnopqrstuvwxyz"
>
> There are 3 bugs I cannot reproduce with the content of the files
> described in the paper:
> ./pr -e t2.txt
> ./md5sum -c t1.txt
> ./ptx x t4.txt
>
> Do you happen to have at hand the content of those files (t1.txt,
> t2.txt and t4.txt)?

I don't have it handy, but there are longer descriptions here:
  http://www.mail-archive.com/coreutils-announce@gnu.org/msg00038.html

> I also tried to use KLEE to find the bugs that I could reproduce on
> the binaries. I tried so far paste, tac and seq.
> I ran KLEE for an hour with the parameters I found in an earlier post.
> I use a version of KLEE from July 2008. I assume this version should
> work too.
>
> Unfortunately, KLEE did not find the bugs. I am not sure if this is
> because of my version of KLEE or due to the parameters I use. Do you
> happen to know the exact parameters I should pass to KLEE for these
> particular coreutils?

I don't have this stuff handy and my memory is fuzzy. May Cristian C. remembers?

 - Daniel

> Thank you,
> Cristi
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>