Go to the documentation of this file.
17 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_ENVIROMENT_H
18 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_ENVIROMENT_H
33 std::shared_ptr<variable_sensitivity_object_factoryt>;
130 std::stack<exprt> remaining_stack,
200 virtual void havoc(
const std::string &havoc_string);
283 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_ENVIROMENT_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual abstract_object_pointert write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
Used within assign to do the actual dispatch.
A map implemented as a tree where subtrees can be shared between different maps.
The type of an expression, extends irept.
abstract_object_pointert resolve_symbol(const exprt &e, const namespacet &ns) const
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
bool verify() const
Check the structural invariants are maintained.
Base class for all expressions.
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print out all the values in the abstract object map.
virtual void havoc(const std::string &havoc_string)
This should be used as a default case / everything else has failed The string is so that I can easily...
Expression to hold a symbol (variable)
void make_top()
Set the domain to top (i.e. everything)
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
virtual abstract_object_pointert eval_expression(const exprt &e, const namespacet &ns) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
variable_sensitivity_object_factory_ptrt object_factory
bool is_top() const
Gets whether the domain is top.
abstract_environmentt(variable_sensitivity_object_factory_ptrt _object_factory)
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.
abstract_environmentt()=delete
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
void make_bottom()
Set the domain to top (i.e. no possible states / unreachable)
sharing_mapt< map_keyt, abstract_object_pointert > map
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 add_object_context(const abstract_object_pointert &abstract_object) const
Wraps an existing object in any configured context object.
virtual bool merge(const abstract_environmentt &env)
Computes the join between "this" and "b".
Statistics gathering for the variable senstivity domain.
This is the basic interface of the abstract interpreter with default implementations of the core func...
static std::vector< abstract_environmentt::map_keyt > modified_symbols(const abstract_environmentt &first, const abstract_environmentt &second)
For our implementation of variable sensitivity domains, we need to be able to efficiently find symbol...
API to expression classes.
abstract_object_statisticst gather_statistics(const namespacet &ns) const
bool is_bottom() const
Gets whether the domain is bottom.
void erase(const symbol_exprt &expr)
Delete a symbol from the map.
virtual bool assume(const exprt &expr, const namespacet &ns)
Reduces the domain based on a condition.