Go to the documentation of this file.
11 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_POINTER_ABSTRACT_OBJECT_H
12 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_POINTER_ABSTRACT_OBJECT_H
105 const std::stack<exprt> &stack,
107 bool merging_write)
const override;
143 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_POINTER_ABSTRACT_OBJECT_H // NOLINT(*)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Print the value of the pointer.
Represents a stack of write operations to an addressable memory location.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
abstract_object_pointert merge_constant_pointers(const constant_pointer_abstract_pointert &other) const
Merges two constant pointers.
abstract_object_pointert merge(abstract_object_pointert op1) const override
Set this abstract object to be the result of merging this abstract object.
The type of an expression, extends irept.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
abstract_object_pointert write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a pointers value.
Base class for all expressions.
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
sharing_ptrt< constant_pointer_abstract_objectt > constant_pointer_abstract_pointert
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
A helper function to dereference a value from a pointer.
exprt to_constant() const override
To try and find a constant expression for this abstract object.
std::set< abstract_object_pointert > abstract_object_visitedt
constant_pointer_abstract_objectt(const typet &type)
The base of all pointer abstractions.
This is the basic interface of the abstract interpreter with default implementations of the core func...
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override