[klee-dev] [klee] [zesti] ZESTI Coreutils Experiments

[Paul Marinescu]

Hello Anton,
From your emails, it doesn't seem that ZESTI is what you're looking for. The paper that you mention is related to KATCH (http://srg.doc.ic.ac.uk/projects/katch/), which is a different project. We don't currently offer KATCH for download but we might do so in the near future; we'll also post early next week a more comprehensive paper on this topic.

If you have further questions specific to KATCH, you can directly send them to me.

Best,
Paul

P.S.
Thanks for spotting the typos on the coreutils page.

On 25 Jun 2013, at 14:52, Anton Vasilyev <anton.vasilyev.87 at gmail.com> wrote:

> 
> 2013/6/25 Jonathan Neuschäfer <j.neuschaefer at gmx.net>
> On Tue, Jun 25, 2013 at 03:41:59PM +0400, Anton Vasilyev wrote:
> > Hello,
> >
> > I'm interesting in integration KLEE with version control (e.g. git).
> > It seems to be similar with project ZESTI.
> 
> You can get a version controlled copy of the KLEE source code either
> with:
>         git clone http://llvm.org/git/klee.git
> or with:
>         svn co http://llvm.org/svn/llvm-project/klee/trunk klee
> 
> I mean not to get klee.git, but integrate patch testing as described at publication "High-Coverage Symbolic Patch Testing" (http://www.doc.ic.ac.uk/~cristic/papers/highcovpatch-spin-12.pdf)
> for native git patch syntax.
> ZESTI project contains "klee_patch_begin()" and "klee_patch_end()" implementation.
> But it is not clear whether ZESTI is the same project relative to the publication.
>  
> [...]
> > 1. Whether it is necessary to replace compiled coreutils-6.11/src with
> > links to installed on system?
> 
> I am not sure what you mean, but the coreutils package installed on your
> system will not be tested by any KLEE or ZESTI experiment.
> 
> This is done by ZESTI provided script at http://srg.doc.ic.ac.uk/projects/zesti/coreutils.html for "setup the wrapper for a particular program and run the tests" by following lines:
> 
>   if [ -x /bin/$fsimple ]; then
>     ln -s /bin/$fsimple
>   elif [ -x /usr/bin/$fsimple ]; then
>     ln -s /usr/bin/$fsimple
> 
> Probably regression tests invoke not only application under testing (as "cut" in example) but also other coreutils binaries.
> In this case it is strange to link system package instead of compile coreutils-6.11 with native gcc at separate location and link these binaries to zesti testing directory.
> 
> > 2. Is it correct that we need to mark patch by functions
> > "klee_patch_begin()" and "klee_patch_end()" for processing by ZESTI ?
> 
> I haven't read enough of the ZESTI source code to answer that question,
> sorry.
> 
> 
> HTH,
> Jonathan Neuschäfer
> 
> 
> 
> -- 
> With best regards,
> Anton Vasilyev

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