13template <
class context_
classt>
18 new context_classt{abstract_object, abstract_object->type()});
21template <
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<liveness_contextt>(abstract_object);
45 return create_context_abstract_object<data_dependency_contextt>(
49 return create_context_abstract_object<write_location_contextt>(
52 return abstract_object;
71template <
class abstract_
object_
classt>
81 auto abstract_object = create_abstract_object<abstract_object_classt>(
82 type, top, bottom, e, environment, ns);
89 const typet &type)
const
94 type.
id() == ID_signedbv || type.
id() == ID_unsignedbv ||
95 type.
id() == ID_fixedbv || type.
id() == ID_c_bool || type.
id() == ID_bool ||
96 type.
id() == ID_integer || type.
id() == ID_c_bit_field)
100 else if(type.
id() == ID_floatbv)
105 else if(type.
id() == ID_array)
109 else if(type.
id() == ID_pointer)
113 else if(type.
id() == ID_struct)
117 else if(type.
id() == ID_union)
121 else if(type.
id() == ID_dynamic_object)
126 return abstract_object_type;
142 switch(abstract_object_type)
145 return initialize_abstract_object<abstract_objectt>(
146 followed_type, top, bottom, e, environment, ns,
configuration);
148 return initialize_abstract_object<constant_abstract_valuet>(
149 followed_type, top, bottom, e, environment, ns,
configuration);
151 return initialize_abstract_object<interval_abstract_valuet>(
152 followed_type, top, bottom, e, environment, ns,
configuration);
154 return initialize_abstract_object<value_set_abstract_objectt>(
155 followed_type, top, bottom, e, environment, ns,
configuration);
158 return initialize_abstract_object<two_value_array_abstract_objectt>(
159 followed_type, top, bottom, e, environment, ns,
configuration);
161 return initialize_abstract_object<full_array_abstract_objectt>(
162 followed_type, top, bottom, e, environment, ns,
configuration);
165 return initialize_abstract_object<two_value_pointer_abstract_objectt>(
166 followed_type, top, bottom, e, environment, ns,
configuration);
168 return initialize_abstract_object<constant_pointer_abstract_objectt>(
169 followed_type, top, bottom, e, environment, ns,
configuration);
171 return initialize_abstract_object<value_set_pointer_abstract_objectt>(
172 followed_type, top, bottom, e, environment, ns,
configuration);
175 return initialize_abstract_object<two_value_struct_abstract_objectt>(
176 followed_type, top, bottom, e, environment, ns,
configuration);
178 return initialize_abstract_object<full_struct_abstract_objectt>(
179 followed_type, top, bottom, e, environment, ns,
configuration);
182 return initialize_abstract_object<two_value_union_abstract_objectt>(
183 followed_type, top, bottom, e, environment, ns,
configuration);
198 return initialize_abstract_object<abstract_objectt>(
199 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.
void set(const irep_idt &name, const irep_idt &value)
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.
Generic base class for unary expressions.
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.
Maintain a context in the variable sensitvity domain that records the liveness region for a given abs...
exprt dynamic_object(const exprt &pointer)
#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
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 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...