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

[Anton Vasilyev]

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