Go to the documentation of this file.
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,
123 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
abstract_object_sett values
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
const_iterator begin() const
The type of an expression, extends irept.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
index_range_ptrt index_range(const namespacet &ns) const override
Base class for all expressions.
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.
std::shared_ptr< index_ranget > index_range_ptrt
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 ...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
value_sett::size_type size() const
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.
an unordered set of value objects
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
virtual exprt to_constant() const
Converts to a constant expression if possible.
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.
const abstract_object_sett & get_values() const override
Getter for the set of stored abstract objects.
abstract_object_pointert to_interval(const abstract_object_sett &other_values) const
Cast the set of values other_values to an interval.
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
value_set_abstract_objectt(const typet &type)
abstract_object_pointert evaluate_conditional(const typet &type, const std::vector< abstract_object_sett > &operands, const abstract_environmentt &env, const namespacet &ns) const
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
Common behaviour for abstract objects modelling values - constants, intervals, etc.