[klee-dev] How to remove the current state from states?

Frank Busse f.busse17 at imperial.ac.uk
Mon Oct 29 11:58:52 GMT 2018


Hi Alberto,


On Fri, 26 Oct 2018 13:41:45 +0100
Alberto Barbaro <barbaro.alberto at gmail.com> wrote:

> I'm on a searcher and I would like to remove the current state from states.
> Should I added it to removedStates or do something else? Can I have the
> example one line code if not too much?  

to gracefully shut down a state in Executor you have to call one
of the terminate functions and afterwards call updateStates() to notify
the searchers. The resp. state is added to removedStates automatically
in terminateState() and removedStates is only used to forward the
information to the searchers. Currently there is no clean way to
terminate a state in a searcher (we discussed that internally a while
ago). What you could do is:

- initialise your searcher with a reference to the executor or
- mark the state (or return tuple in select() etc.) and adapt the main
  interpreter loop (select/delete until un-marked state found)

The 2nd option is less error-prone.


Kind regards,

Frank




More information about the klee-dev mailing list