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 <[email protected]> wrote: > > 2013/6/25 Jonathan Neuschäfer <[email protected]> > 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
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
