Hello, Anton. > But it is not clear whether ZESTI is the same project relative to the > publication.
Maybe it is worth to investigate ZESTI a little more? Project page is http://srg.doc.ic.ac.uk/projects/zesti/ Some additional information can be surely found at http://www.doc.ic.ac.uk/~cristic/papers/zesti-icse-12.pdf This can really improve your progress with integration, Urmas Repinski. Date: Tue, 25 Jun 2013 17:52:36 +0400 From: [email protected] To: [email protected] CC: [email protected] Subject: Re: [klee-dev] [klee] [zesti] ZESTI Coreutils Experiments 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
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
