13 template <
class context_
classt>
18 new context_classt{abstract_object, abstract_object->type()});
21 template <
class abstract_
object_
classt>
31 return std::make_shared<abstract_object_classt>(type, top, bottom);
34 return std::make_shared<abstract_object_classt>(e, environment, ns);
42 return create_context_abstract_object<data_dependency_contextt>(
46 return create_context_abstract_object<write_location_contextt>(
49 return abstract_object;
67 template <
class abstract_
object_
classt>
77 auto abstract_object = create_abstract_object<abstract_object_classt>(
78 type, top, bottom, e, environment, ns);
85 const typet &type)
const
90 type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
91 type.
id() == ID_fixedbv || type.
id() == ID_c_bool || type.
id() == ID_bool ||
92 type.
id() == ID_integer || type.
id() == ID_c_bit_field)
96 else if(type.
id() == ID_floatbv)
101 else if(type.
id() == ID_array)
105 else if(type.
id() == ID_pointer)
109 else if(type.
id() == ID_struct)
113 else if(type.
id() == ID_union)
118 return abstract_object_type;
134 switch(abstract_object_type)
137 return initialize_abstract_object<abstract_objectt>(
138 followed_type, top, bottom, e, environment, ns,
configuration);
140 return initialize_abstract_object<constant_abstract_valuet>(
141 followed_type, top, bottom, e, environment, ns,
configuration);
143 return initialize_abstract_object<interval_abstract_valuet>(
144 followed_type, top, bottom, e, environment, ns,
configuration);
148 return initialize_abstract_object<value_set_abstract_valuet>(
149 followed_type, top, bottom, e, environment, ns,
configuration);
151 return initialize_abstract_object<value_set_abstract_objectt>(
152 followed_type, top, bottom, e, environment, ns,
configuration);
155 return initialize_abstract_object<two_value_array_abstract_objectt>(
156 followed_type, top, bottom, e, environment, ns,
configuration);
158 return initialize_abstract_object<full_array_abstract_objectt>(
159 followed_type, top, bottom, e, environment, ns,
configuration);
162 return initialize_abstract_object<two_value_pointer_abstract_objectt>(
163 followed_type, top, bottom, e, environment, ns,
configuration);
165 return initialize_abstract_object<constant_pointer_abstract_objectt>(
166 followed_type, top, bottom, e, environment, ns,
configuration);
168 return initialize_abstract_object<value_set_pointer_abstract_objectt>(
169 followed_type, top, bottom, e, environment, ns,
configuration);
172 return initialize_abstract_object<two_value_struct_abstract_objectt>(
173 followed_type, top, bottom, e, environment, ns,
configuration);
175 return initialize_abstract_object<full_struct_abstract_objectt>(
176 followed_type, top, bottom, e, environment, ns,
configuration);
179 return initialize_abstract_object<two_value_union_abstract_objectt>(
180 followed_type, top, bottom, e, environment, ns,
configuration);
184 return initialize_abstract_object<abstract_objectt>(
185 followed_type, top, bottom, e, environment, ns,
configuration);
sharing_ptrt< class abstract_objectt > abstract_object_pointert
floatbv_typet float_type()
Base class for all expressions.
typet & type()
Return the type of the expression.
const irep_idt & id() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The type of an expression, extends irept.
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.
abstract_object_pointert wrap_with_context(const abstract_object_pointert &abstract_object) const
vsd_configt configuration
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 an array value.
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
ABSTRACT_OBJECT_TYPET union_abstract_type
struct vsd_configt::@0 context_tracking
struct vsd_configt::@1 advanced_sensitivities
ABSTRACT_OBJECT_TYPET pointer_abstract_type
bool data_dependency_context
ABSTRACT_OBJECT_TYPET struct_abstract_type
ABSTRACT_OBJECT_TYPET array_abstract_type
ABSTRACT_OBJECT_TYPET value_abstract_type
Value sets for primitives.
Value Set of Pointer Abstract Object.
abstract_object_pointert create_context_abstract_object(const abstract_object_pointert &abstract_object)
abstract_object_pointert initialize_abstract_object(const typet type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns, const vsd_configt &configuration)
Function: variable_sensitivity_object_factoryt::initialize_abstract_object Initialize the abstract ob...
abstract_object_pointert create_abstract_object(const typet type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns)
abstract_object_pointert wrap_with_context_object(const abstract_object_pointert &abstract_object, const vsd_configt &configuration)
Tracks the user-supplied configuration for VSD and build the correct type of abstract object when nee...