12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
49 const std::vector<abstract_object_pointert> &operands,
74 const std::stack<exprt> &stack,
75 const exprt &specifier,
77 bool merging_write)
const override;
91 const std::vector<abstract_object_sett> &operands,
sharing_ptrt< class abstract_objectt > abstract_object_pointert
an unordered set of value objects
Common behaviour for abstract objects modelling values - constants, intervals, etc.
std::shared_ptr< index_ranget > index_range_ptrt
const_iterator begin() const
value_sett::size_type size() const
virtual exprt to_constant() const
Converts to a constant expression if possible.
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
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.
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.
index_range_ptrt index_range(const namespacet &ns) const override
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
abstract_object_pointert resolve_new_values(const abstract_object_sett &new_values, const abstract_environmentt &environment) const
Update the set of stored values to new_values.
const abstract_object_sett & get_values() const override
Getter for the set of stored abstract objects.
abstract_object_sett values
static const size_t max_value_set_size
The threshold size for value-sets: past this threshold the object is either converted to interval or ...
abstract_object_pointert to_interval(const abstract_object_sett &other_values) const
Cast the set of values other_values to an interval.
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
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.
value_set_abstract_objectt(const typet &type)
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_object_pointert evaluate_conditional(const typet &type, const std::vector< abstract_object_sett > &operands, const abstract_environmentt &env, const namespacet &ns) const