ai_domain_baset()
The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the d...
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
virtual const locationt & current_location(void) const =0
The current location in the history, used to compute the transformer POSTCONDITION(return value is de...
This is the domain for a value set analysis.
xmlt output_xml(const ai_baset &ai, const namespacet &ns) const override
exprt get_return_lhs(locationt to) const
void get_reference_set(const namespacet &ns, const exprt &expr, value_setst::valuest &dest)
bool merge(const value_set_domain_templatet< VST > &other, trace_ptrt, trace_ptrt)
void make_entry() override
Make this domain a reasonable entry-point state For most domains top is sufficient.
void make_bottom() override
no states
bool is_top() const override
value_set_domain_templatet(locationt l)
void transform(const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt to, ai_baset &ai, const namespacet &ns) override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
bool is_bottom() const override
void output(std::ostream &out, const ai_baset &, const namespacet &) const override
void make_top() override
all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implem...
ai_domain_factory_location_constructort< value_set_domaint > value_set_domain_factoryt
value_set_domain_templatet< value_sett > value_set_domaint