CBMC
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 {
27 public:
29  configured_with(const vsd_configt &options)
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 
62  wrap_with_context(const abstract_object_pointert &abstract_object) const;
63 
66  const variable_sensitivity_object_factoryt &) = delete;
67 
68  const vsd_configt &config() const
69  {
70  return configuration;
71  }
72 
73 private:
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
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:94
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.
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...