[klee-dev] Target-Directed Symbolic Execution with KLEE

[Papapanagiotakis-Bousy, Iason]

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-bounces at imperial.ac.uk [mailto:klee-dev-bounces at imperial.ac.uk] On Behalf Of Yannic Noller
Sent: Monday, January 23, 2017 2:54 PM
To: klee-dev at 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
-------------- next part --------------
HTML attachment scrubbed and removed