CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
18#include "abstract_object.h"
20
23 std::shared_ptr<variable_sensitivity_object_factoryt>;
24
26{
27public:
30 {
31 return std::make_shared<variable_sensitivity_object_factoryt>(options);
32 }
33
35 : configuration{options}, heap_allocations(0)
36 {
37 }
38
54 const typet &type,
55 bool top,
56 bool bottom,
57 const exprt &e,
58 const abstract_environmentt &environment,
59 const namespacet &ns) const;
60
63
67
68 const vsd_configt &config() const
69 {
70 return configuration;
71 }
72
73private:
81
83 mutable size_t heap_allocations;
84};
85
86#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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
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 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.
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