26 : t(type), bottom(false), top(true)
31 : t(type), bottom(bottom), top(top)
40 : t(expr.type()), bottom(false), top(true)
49 : t(type), bottom(false), top(true)
67 if(
is_top() || other->bottom)
72 merged->bottom =
false;
73 return merged->abstract_object_merge_internal(other);
80 return shared_from_this();
98 return met->abstract_object_meet_internal(other);
105 return shared_from_this();
110 const std::vector<abstract_object_pointert> &operands,
119 const exprt &const_op = op_abstract_object->to_constant();
120 op = const_op.
is_nil() ? op : const_op;
128 const exprt &const_op = op_abstract_object->to_constant();
142 const std::stack<exprt> &stack,
143 const exprt &specifier,
145 bool merging_write)
const
192 bool &out_modifications)
195 ? op1->abstract_object_merge(op2)
198 out_modifications = result != op1;
208 return merge(op1, op2, dummy);
214 return is_top() || other->is_bottom() || other->is_top();
220 bool &out_modifications)
223 ? op1->abstract_object_meet(op2)
226 out_modifications = result != op1;
234 return is_bottom() || other->is_bottom() || other->is_top();
239 const bool update_sub_elements)
const
241 return shared_from_this();
253 for(
auto &item : view)
255 out << (first ?
"" :
", ") << item.first;
271 for(
auto &item : delta_view)
273 out << (first ?
"" :
", ") << item.k <<
"=" << item.is_in_both_maps();
281 return shared_from_this();
290 const auto &this_ptr = shared_from_this();
292 visited.insert(this_ptr);
An abstract version of a program environment.
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
virtual exprt to_constant() const
Converts to a constant expression if possible.
static abstract_object_pointert meet(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Interface method for the meet operation.
abstract_objectt(const typet &type)
virtual bool is_top() const
Find out if the abstract object is top.
static void dump_map(std::ostream out, const shared_mapt &m)
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
virtual 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
A helper function to evaluate writing to a component of an abstract object.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual internal_abstract_object_pointert mutable_clone() const
virtual abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
Interface for transforms.
bool should_use_base_meet(const abstract_object_pointert &other) const
Helper function to decide if base meet implementation should be used.
virtual abstract_object_pointert abstract_object_meet_internal(const abstract_object_pointert &other) const
Helper function for base meet, in case additional work was needed.
static void dump_map_diff(std::ostream out, const shared_mapt &m1, const shared_mapt &m2)
Dump all elements in m1 that are different or missing in m2.
abstract_object_pointert abstract_object_merge(const abstract_object_pointert other) const
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
virtual abstract_object_pointert update_location_context(const locationst &locations, const bool update_sub_elements) const
Update the location context for an abstract object, potentially propogating the update to any childre...
bool should_use_base_merge(const abstract_object_pointert other) const
To detect the cases where the base merge is sufficient to do a merge We can't do if this->is_bottom()...
abstract_object_pointert abstract_object_meet(const abstract_object_pointert &other) const
Helper function for base meet.
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
virtual abstract_object_pointert abstract_object_merge_internal(const abstract_object_pointert other) const
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after t...
internal_sharing_ptrt< class abstract_objectt > internal_abstract_object_pointert
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
virtual abstract_object_pointert unwrap_context() const
std::set< goto_programt::const_targett > locationst
typet t
To enforce copy-on-write these are private and have read-only accessors.
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Base class for all expressions.
typet & type()
Return the type of the expression.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
void get_delta_view(const sharing_mapt &other, delta_viewt &delta_view, const bool only_common=true) const
Get a delta view of the elements in the map.
void get_view(V &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
The type of an expression, extends irept.
An abstraction of a single value that just stores a constant.
bool simplify(exprt &expr, const namespacet &ns)
#define PRECONDITION(CONDITION)
API to expression classes.
Defines typet, type_with_subtypet and type_with_subtypest.