12#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H
13#define CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H
38 value_set.location_number = l->location_number;
73 return value_set.make_union(other.value_set);
95 value_set.get_reference_set(expr, dest, ns);
103 if(
to->is_end_function())
106 INVARIANT(
to->is_function_call(),
"must be the function call");
108 return to->call_lhs();
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);
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
virtual void clear()
Reset the abstract state.
virtual xmlt output_xml(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
Output the abstract states for a single function as XML.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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...
std::list< exprt > valuest
const irept & get_nil_irep()
#define UNREACHABLE
This should be used to mark dead code.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
ai_domain_factory_location_constructort< value_set_domaint > value_set_domain_factoryt
value_set_domain_templatet< value_sett > value_set_domaint