Hi Cristian, thanks for the hint, I will take a look.
— Yannic > On 25 Jan 2017, at 16:01, Cristian Cadar <[email protected]> wrote: > > Hi Yannic, you might like to take a look at KATCH: > http://srg.doc.ic.ac.uk/projects/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 >>> <[email protected] >>> <mailto:[email protected] >>> <mailto:[email protected]>>> wrote: >>> >>> Hi Yannic, >>> >>> Have you looked into the maze >>> tutorial https://feliam.wordpress.com/2010/10/07/the-symbolic-maze/ >>> <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:* [email protected] >>> <mailto:[email protected]> >>> <mailto:[email protected] >>> <mailto:[email protected]>> >>> [mailto:[email protected] >>> <mailto:[email protected]>] *On Behalf Of *Yannic Noller >>> *Sent:* Monday, January 23, 2017 2:54 PM >>> *To:* [email protected] <mailto:[email protected]> >>> <mailto:[email protected] <mailto:[email protected]>> >>> *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 >> [email protected] <mailto:[email protected]> >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> >> > > _______________________________________________ > klee-dev mailing list > [email protected] <mailto:[email protected]> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
