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

[Urmas Repinski]

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: anton.vasilyev.87 at gmail.com
To: j.neuschaefer at gmx.net
CC: klee-dev at imperial.ac.uk
Subject: Re: [klee-dev] [klee] [zesti] ZESTI Coreutils Experiments


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


_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed