8#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONTEXT_ABSTRACT_OBJECT_H
9#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONTEXT_ABSTRACT_OBJECT_H
72 const std::vector<abstract_object_pointert> &operands,
103 std::shared_ptr<context_abstract_objectt>;
118 const std::stack<exprt> &stack,
119 const exprt &specifier,
121 bool merging_write)
const override;
127 typedef std::set<locationt, goto_programt::target_less_than>
locationst;
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
goto_programt::const_targett locationt
abstract_objectt(const typet &type, bool top, bool bottom)
Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true.
This is the basic interface of the abstract interpreter with default implementations of the core func...
bool is_bottom() const override
Find out if the abstract object is bottom.
virtual context_abstract_object_ptrt update_location_context_internal(const locationst &locations) const =0
abstract_object_pointert write_location_context(const locationt &location) const override
Update the location context for an abstract object.
std::shared_ptr< context_abstract_objectt > context_abstract_object_ptrt
abstract_object_pointert envelop(abstract_object_pointert &child) const
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.
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...
context_abstract_objectt(const abstract_object_pointert child, const typet &type, bool top, bool bottom)
context_abstract_objectt(const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
virtual ~context_abstract_objectt()
abstract_object_pointert child_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
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.
std::set< locationt, goto_programt::target_less_than > locationst
bool is_top() const override
Find out if the abstract object is top.
exprt to_constant() const override
Converts to a constant expression if possible.
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
const typet & type() const override
Get the real type of the variable this abstract object is representing.
abstract_object_pointert unwrap_context() const override
void set_not_top_internal() override
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
Base class for all expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The type of an expression, extends irept.