131 locationt from_l{from->current_location()};
134 switch(from_l->type())
142 value_set.do_end_function(get_return_lhs(to_l), ns);
152 value_set.apply_code(from_l->code(), ns);
156 value_set.guard(from_l->condition(), ns);
160 value_set.do_function_call(function_to, from_l->call_arguments(), ns);
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
goto_programt::const_targett locationt
ai_history_baset::trace_ptrt trace_ptrt
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)
bool reachable
ait checks whether domains are bottom to increase speed and accuracy.
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