Hi Yannic, you might like to take a look at KATCH:
http://srg.doc.ic.ac.uk/projects/katch/
The code is available, but unfortunately not integrated into the mainline.
Cristian
On 23/01/17 15:31, Yannic Noller wrote:
Hi Jason,
thanks, I know the example and you are right: this is probably the
fastest way to try my idea. But this means that there is no special
option for an target-oriented search, right? For example I do not want
to follow paths that cannot reach my specified target line in order to
cut down the possible state space. If not, is it easy to implement such
a feature in KLEE?
Thanks!
— Yannic
On 23 Jan 2017, at 14:12, Papapanagiotakis-Bousy, Iason
<iason.papapanagiotakis-bousy...@ucl.ac.uk
<mailto:iason.papapanagiotakis-bousy...@ucl.ac.uk>> wrote:
Hi Yannic,
Have you looked into the maze
tutorial https://feliam.wordpress.com/2010/10/07/the-symbolic-maze/ ?
I am no KLEE veteran but here is my suggestion:
If I understand correctly what you are trying to achieve, then you
could use what is shown in the tutorial and at the end instead of
looking at the .ktest files that will have concrete examples, read the
corresponding .kquery files that contain the path constraints.
(because the tutorial uses an older version of KLEE, constraints are
stored in a .pc instead of .kquery)
Hope it helps.
Best regards,
Jason
*From:* klee-dev-boun...@imperial.ac.uk
<mailto:klee-dev-boun...@imperial.ac.uk>
[mailto:klee-dev-boun...@imperial.ac.uk] *On Behalf Of *Yannic Noller
*Sent:* Monday, January 23, 2017 2:54 PM
*To:* klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
*Subject:* [klee-dev] Target-Directed Symbolic Execution with KLEE
Hi all,
I would like to create all path conditions (or an under-approximation)
that reach a certain source code line (something like "directed
symbolic execution"). Is there an option in KLEE to do that? Or is
there an extension of KLEE that can do that?
Any help is very appreciated :)
Thanks,
Yannic
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
