Thanks Martin, I think tipically within the update function all the states within the 'removedStates' vector are removed from the 'states' variable so I thought I should do the same in my case.
If in other cases states are added I think my approach to remove or add states depending on the condition described in the .path file it would not work. Are you happy to describe an approach that I should use for creating this kind of searcher? Just to clarify, I have a ,path file with 0's and 1's because a program was executed with a real input file as parameter and now I would like to execute again the same program but with symbolic input and be able to follow exactly the same path had before. Thanks On Wed, May 2, 2018, 22:11 Nowack, Martin <[email protected]> wrote: > Hi Alberto, > > The function `selectState()` returns the state you would like KLEE to work > on next. > So this always only one state. > > The update function is KLEE’s callback to your searcher to inform you > which states have been added or removed. > > But, you should not make any assumption on the order of states coming in > nor how many states you will have. > Forking of states can happen at different positions not only the branch > instruction. > > The only information you can currently consider as exact is the one you > get from the state itself: e.g. the old > instruction pointer and the new instruction pointer, but of course there > is much more there. > > Hope that helps you a bit further. > > Best, > Martin > > On 2. May 2018, at 20:16, Alberto Barbaro <[email protected]> > wrote: > > Hi all, > thanks for the answer. I was able to create another searcher called > "guided" that should do what i want but I have problem for now. From my > understanding the crucial function to implement are: update and selectState. > > I think in the selectState function I should return *states[0] or > *states[1] depending if in the condition is false or true. I'm not sure > that the first state represents the false condition so please let me know > if I'm wrong. Instead, within the update function I should remove all the > states apart states[0] or states[1] depending on the content of the file > again. > > Unfortunately I'm not sure that if my idea is correct. Can someone let me > know what I'm missing and maybe give me an example? > > Thanks > Alberto > > On Sun, Mar 18, 2018, 19:31 Cristian Cadar <[email protected]> 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 >> > [email protected] >> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> > >> >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
