Skip to content

Commit 4acb533

Browse files
committed
Move heap object creation off into object factory.
This feels like the right place for this, and also gives future options for configuration/customisation.
1 parent a2e8439 commit 4acb533

File tree

3 files changed

+20
-8
lines changed

3 files changed

+20
-8
lines changed

src/analyses/variable-sensitivity/abstract_environment.cpp

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -88,13 +88,10 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
8888
simplified_id == ID_side_effect &&
8989
(simplified_expr.get(ID_statement) == ID_allocate))
9090
{
91-
auto dynamic_object = exprt(ID_dynamic_object);
92-
dynamic_object.set(ID_identifier, "allocated-on-heap");
93-
auto heap_symbol =
94-
unary_exprt(ID_address_of, dynamic_object, simplified_expr.type());
95-
auto heap_pointer =
96-
abstract_object_factory(simplified_expr.type(), heap_symbol, ns);
97-
return heap_pointer;
91+
return abstract_object_factory(
92+
typet(ID_dynamic_object),
93+
exprt(ID_dynamic_object, simplified_expr.type()),
94+
ns);
9895
}
9996

10097
// No special handling required by the abstract environment

src/analyses/variable-sensitivity/variable_sensitivity_configuration.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,8 @@ enum ABSTRACT_OBJECT_TYPET
3131
STRUCT_INSENSITIVE,
3232
// TODO: plug in UNION_SENSITIVE HERE
3333
UNION_INSENSITIVE,
34-
VALUE_SET
34+
VALUE_SET,
35+
HEAP_ALLOCATION
3536
};
3637

3738
enum class flow_sensitivityt

src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,10 @@ variable_sensitivity_object_factoryt::get_abstract_object_type(
114114
{
115115
return configuration.union_abstract_type;
116116
}
117+
else if(type.id() == ID_dynamic_object)
118+
{
119+
return HEAP_ALLOCATION;
120+
}
117121

118122
return abstract_object_type;
119123
}
@@ -174,6 +178,16 @@ variable_sensitivity_object_factoryt::get_abstract_object(
174178
return initialize_abstract_object<two_value_union_abstract_objectt>(
175179
followed_type, top, bottom, e, environment, ns, configuration);
176180

181+
case HEAP_ALLOCATION:
182+
{
183+
auto dynamic_object = exprt(ID_dynamic_object);
184+
dynamic_object.set(ID_identifier, "allocated-on-heap");
185+
auto heap_symbol = unary_exprt(ID_address_of, dynamic_object, e.type());
186+
auto heap_pointer =
187+
get_abstract_object(e.type(), false, false, heap_symbol, environment, ns);
188+
return heap_pointer;
189+
}
190+
177191
default:
178192
UNREACHABLE;
179193
return initialize_abstract_object<abstract_objectt>(

0 commit comments

Comments
 (0)