virtual void make_bottom()=0
no states
virtual void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns)=0
how function calls are treated: a) there is an edge from each call site to the function head b) there...
virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const
virtual bool is_bottom() const =0
ai_domain_baset()
The constructor is expected to produce 'false' or 'bottom'.
virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const
Simplifies the expression but keeps it as an l-value.
virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const
virtual ~ai_domain_baset()
goto_programt::const_targett locationt
virtual exprt to_predicate(void) const
Gives a Boolean condition that is true for all values represented by the domain.
virtual void make_entry()=0
Make this domain a reasonable entry-point state.
virtual bool is_top() const =0
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
virtual void output(std::ostream &, const ai_baset &, const namespacet &) const
virtual void make_top()=0
all states – the analysis doesn't use this, and domains may refuse to implement it.