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: [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
