abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Try to resolve an expression with the maximum level of precision available.
void set_top_internal() override
context_abstract_objectt(const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
Output a representation of the value of this abstract object.
context_abstract_objectt(const abstract_object_pointert child, const typet &type)
abstract_object_pointert get_child() const
abstract_object_pointert unwrap_context() const override
bool is_top() const override
Find out if the abstract object is top.
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
void set_not_top_internal() override
CLONE abstract_object_pointert child_abstract_object
const typet & type() const override
Get the real type of the variable this abstract object is representing.
bool has_been_modified(const abstract_object_pointert before) const override
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state...
virtual ~context_abstract_objectt()
bool is_bottom() const override
Find out if the abstract object is bottom.
context_abstract_objectt(const abstract_object_pointert child, const typet &type, bool top, bool bottom)
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
void set_child(const abstract_object_pointert &child)
exprt to_constant() const override
Converts to a constant expression if possible.