[klee-dev] How to introduce the "Exploration Technique" concept

[Alberto Barbaro]

Thanks I'll do, do you think my approach is correct or should I do it on a
different way? How would you approach it?

Thanks

On Sun, Mar 18, 2018, 19:31 Cristian Cadar <c.cadar at imperial.ac.uk> wrote:

> My recommendation is to implement such an exploration technique as an
> independent search heuristic.  The bar for changing the core of KLEE is
> much higher, as it affects all users.
>
> Best,
> Cristian
>
> On 18/03/2018 17:41, Alberto Barbaro wrote:
> > Hi,
> > I'm working on a possible PULL request that would allow to execute a
> > project but excluding paths based on a .path previously generated using
> > KLEE. Doing so it would be possible to have some sort of "exploration
> > technique" that would help to follow specific paths.
> >
> > I think, after having generated the .path file, it would be possible to
> > do so amending Executor.cpp main switch for the Instruction::Br case.
> > I'm able to keep track of the "index" for the current branch so I would
> > check cond.get().isTrue() comparing with value on line "index". At this
> > point I'm not sure how to skip a branch ( I cannot use exit(0) like
> > klee_silent_exit I think ). Should I just modify the if for the "br"
> > branch of the switch?
> >
> > Thanks for any suggesiton,
> > A
> >
> >
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at imperial.ac.uk
> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> >
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed