cprover
Loading...
Searching...
No Matches
variable_sensitivity_object_factory.h
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Owen Jones owen.jones@diffblue.com
6
7\*******************************************************************/
8
14
15#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_OBJECT_FACTORY_H
16#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_OBJECT_FACTORY_H
17
30
31#include "abstract_object.h"
32
35 std::shared_ptr<variable_sensitivity_object_factoryt>;
36
38{
39public:
42 {
43 return std::make_shared<variable_sensitivity_object_factoryt>(options);
44 }
45
47 : configuration{options}, heap_allocations(0)
48 {
49 }
50
66 const typet &type,
67 bool top,
68 bool bottom,
69 const exprt &e,
70 const abstract_environmentt &environment,
71 const namespacet &ns) const;
72
74 wrap_with_context(const abstract_object_pointert &abstract_object) const;
75
79
80 const vsd_configt &config() const
81 {
82 return configuration;
83 }
84
85private:
93
95 mutable size_t heap_allocations;
96};
97
98#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_OBJECT_FACTORY_H // NOLINT(*)
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Base class for all expressions.
Definition: expr.h:54
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The type of an expression, extends irept.
Definition: type.h:29
abstract_object_pointert get_abstract_object(const typet &type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns) const
Get the appropriate abstract object for the variable under consideration.
variable_sensitivity_object_factoryt(const vsd_configt &options)
variable_sensitivity_object_factoryt(const variable_sensitivity_object_factoryt &)=delete
abstract_object_pointert wrap_with_context(const abstract_object_pointert &abstract_object) const
static variable_sensitivity_object_factory_ptrt configured_with(const vsd_configt &options)
ABSTRACT_OBJECT_TYPET get_abstract_object_type(const typet &type) const
Decide which abstract object type to use for the variable in question.
An abstraction of a single value that just stores a constant.
An abstraction of a pointer that tracks a single pointer.
Maintain data dependencies as a context in the variable sensitivity domain.
An abstraction of a structure that stores one abstract object per field.
An interval to represent a set of possible values.
The base type of all abstract array representations.
The base of all structure abstractions.
The base of all union abstractions.
Value Set Abstract Object.
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
Maintain a context in the variable sensitvity domain that records write locations for a given abstrac...