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]> 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]] On Behalf Of Yannic Noller > Sent: Monday, January 23, 2017 2:54 PM > To: [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] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
