52 const std::stack<exprt> &stack,
53 const exprt &specifier,
55 bool merging_write)
const
58 environment, ns, stack, specifier, value, merging_write);
62 return shared_from_this();
66 std::dynamic_pointer_cast<context_abstract_objectt>(
mutable_clone());
69 result->set_child(updated_child);
88 const std::vector<abstract_object_pointert> &operands,
94 std::vector<abstract_object_pointert> child_operands;
99 std::back_inserter(child_operands),
101 PRECONDITION(op != nullptr);
102 auto p = std::dynamic_pointer_cast<const context_abstract_objectt>(op);
103 INVARIANT(p,
"Operand shall be of type context_abstract_objectt");
104 return p->child_abstract_object;
108 expr, child_operands, environment, ns);
141 auto before_context =
142 std::dynamic_pointer_cast<const context_abstract_objectt>(before);
145 before_context->child_abstract_object.get();
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual internal_abstract_object_pointert mutable_clone() const
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
This is the basic interface of the abstract interpreter with default implementations of the core func...
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.
void set_child(const abstract_object_pointert &child)
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
CLONE abstract_object_pointert child_abstract_object
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.
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_top_internal() override
abstract_object_pointert get_child() const
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...
abstract_object_pointert unwrap_context() const override
void set_not_top_internal() override
Base class for all expressions.
static memory_sizet from_bytes(std::size_t bytes)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
#define PRECONDITION(CONDITION)
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.