Skip to content

Commit 814ca07

Browse files
author
Owen
committed
Remove redundant ID_dynamic_object branch
This branch is not taken any more, at least in symex. The code in it doesn't make much sense, which makes me think it isn't taken at all.
1 parent dc4611f commit 814ca07

File tree

1 file changed

+0
-18
lines changed

1 file changed

+0
-18
lines changed

src/pointer-analysis/value_set_dereference.cpp

Lines changed: 0 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -291,24 +291,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
291291
result.ignore = true;
292292
}
293293
}
294-
else if(root_object.id()==ID_dynamic_object)
295-
{
296-
// const dynamic_object_exprt &dynamic_object=
297-
// to_dynamic_object_expr(root_object);
298-
299-
// the object produced by malloc
300-
exprt malloc_object=
301-
ns.lookup(CPROVER_PREFIX "malloc_object").symbol_expr();
302-
303-
exprt is_malloc_object=same_object(pointer_expr, malloc_object);
304-
305-
// constraint that it actually is a dynamic object
306-
// this is also our guard
307-
result.pointer_guard = dynamic_object(pointer_expr);
308-
309-
// can't remove here, turn into *p
310-
result.value=dereference_exprt(pointer_expr, dereference_type);
311-
}
312294
else if(root_object.id()==ID_integer_address)
313295
{
314296
// This is stuff like *((char *)5).

0 commit comments

Comments
 (0)