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

[Yannic Noller]

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.15 at ucl.ac.uk> 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: 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