cprover
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 
32 #include <util/namespace.h>
33 
36  std::shared_ptr<variable_sensitivity_object_factoryt>;
37 
39 {
40 public:
42  configured_with(const vsd_configt &options)
43  {
44  return std::make_shared<variable_sensitivity_object_factoryt>(options);
45  }
46 
48  : configuration{options}
49  {
50  }
51 
67  const typet &type,
68  bool top,
69  bool bottom,
70  const exprt &e,
71  const abstract_environmentt &environment,
72  const namespacet &ns) const;
73 
75  wrap_with_context(const abstract_object_pointert &abstract_object) const;
76 
79  const variable_sensitivity_object_factoryt &) = delete;
80 
81 private:
89 
91 };
92 
93 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_OBJECT_FACTORY_H // NOLINT(*)
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
typet
The type of an expression, extends irept.
Definition: type.h:28
context_abstract_object.h
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
two_value_struct_abstract_object.h
The base of all structure abstractions.
variable_sensitivity_object_factoryt::variable_sensitivity_object_factoryt
variable_sensitivity_object_factoryt(const variable_sensitivity_object_factoryt &)=delete
variable_sensitivity_object_factoryt::wrap_with_context
abstract_object_pointert wrap_with_context(const abstract_object_pointert &abstract_object) const
Definition: variable_sensitivity_object_factory.cpp:190
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
write_location_context.h
Maintain a context in the variable sensitvity domain that records write locations for a given abstrac...
variable_sensitivity_object_factoryt::get_abstract_object_type
ABSTRACT_OBJECT_TYPET get_abstract_object_type(const typet &type) const
Decide which abstract object type to use for the variable in question.
Definition: variable_sensitivity_object_factory.cpp:84
variable_sensitivity_object_factoryt::variable_sensitivity_object_factoryt
variable_sensitivity_object_factoryt(const vsd_configt &options)
Definition: variable_sensitivity_object_factory.h:47
namespace.h
vsd_configt
Definition: variable_sensitivity_configuration.h:41
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
full_struct_abstract_object.h
An abstraction of a structure that stores one abstract object per field.
two_value_pointer_abstract_object.h
variable_sensitivity_object_factoryt::variable_sensitivity_object_factoryt
variable_sensitivity_object_factoryt()=delete
value_set_abstract_object.h
Value Set Abstract Object.
variable_sensitivity_object_factory_ptrt
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
Definition: abstract_environment.h:33
constant_pointer_abstract_object.h
An abstraction of a pointer that tracks a single pointer.
full_array_abstract_object.h
An abstraction of an array value.
data_dependency_context.h
Maintain data dependencies as a context in the variable sensitivity domain.
variable_sensitivity_object_factoryt
Definition: variable_sensitivity_object_factory.h:39
two_value_union_abstract_object.h
The base of all union abstractions.
variable_sensitivity_object_factoryt::configuration
vsd_configt configuration
Definition: variable_sensitivity_object_factory.h:90
interval_abstract_value.h
An interval to represent a set of possible values.
variable_sensitivity_object_factoryt::get_abstract_object
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.
Definition: variable_sensitivity_object_factory.cpp:122
two_value_array_abstract_object.h
The base type of all abstract array representations.
ABSTRACT_OBJECT_TYPET
ABSTRACT_OBJECT_TYPET
Definition: variable_sensitivity_configuration.h:18
variable_sensitivity_configuration.h
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...
constant_abstract_value.h
An abstraction of a single value that just stores a constant.
variable_sensitivity_object_factoryt::configured_with
static variable_sensitivity_object_factory_ptrt configured_with(const vsd_configt &options)
Definition: variable_sensitivity_object_factory.h:42