Go to the documentation of this file.
37 "Abstract states are only merged at reachable locations");
58 "Transformers are only applied at reachable locations");
60 if(from->is_start_thread())
85 "A location cannot be threaded if it is not reachable.");
104 is_threaded_analysis(goto_functions, ns);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void make_bottom() final override
no states
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
virtual cstate_ptrt abstract_state_before(locationt l) const
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
void make_entry() final override
Make this domain a reasonable entry-point state.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
bool is_bottom() const override final
Over-approximate Concurrency for Threaded Goto Programs.
void compute(const goto_functionst &goto_functions)
void transform(const irep_idt &, locationt from, const irep_idt &, locationt, ai_baset &, const namespacet &) final override
is_threaded_sett is_threaded_set
bool is_top() const override final
A collection of goto functions.
goto_programt::const_targett locationt
This is the basic interface of the abstract interpreter with default implementations of the core func...
bool merge(const is_threaded_domaint &src, locationt, locationt)
#define forall_goto_functions(it, functions)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
#define forall_goto_program_instructions(it, program)