Skip to content

Commit bb29057

Browse files
committed
Remove deprecated dynamic_object pointer predicate
It has been marked deprecated for more than six months. Any uses outside the code base should use is_dynamic_object_exprt.
1 parent 8562df3 commit bb29057

File tree

3 files changed

+1
-11
lines changed

3 files changed

+1
-11
lines changed

src/pointer-analysis/value_set_dereference.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -480,7 +480,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
480480
{
481481
// constraint that it actually is a dynamic object
482482
// this is also our guard
483-
result.pointer_guard = dynamic_object(pointer_expr);
483+
result.pointer_guard = is_dynamic_object_exprt(pointer_expr);
484484

485485
// can't remove here, turn into *p
486486
result.value = dereference_exprt{pointer_expr};

src/util/pointer_predicates.cpp

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -56,13 +56,6 @@ exprt dead_object(const exprt &pointer, const namespacet &ns)
5656
return same_object(pointer, deallocated_symbol.symbol_expr());
5757
}
5858

59-
exprt dynamic_object(const exprt &pointer)
60-
{
61-
exprt dynamic_expr(ID_is_dynamic_object, bool_typet());
62-
dynamic_expr.copy_to_operands(pointer);
63-
return dynamic_expr;
64-
}
65-
6659
exprt good_pointer(const exprt &pointer)
6760
{
6861
return unary_exprt(ID_good_pointer, pointer, bool_typet());

src/util/pointer_predicates.h

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_UTIL_POINTER_PREDICATES_H
1313
#define CPROVER_UTIL_POINTER_PREDICATES_H
1414

15-
#include "deprecate.h"
1615
#include "std_expr.h"
1716

1817
#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
@@ -23,8 +22,6 @@ exprt dead_object(const exprt &pointer, const namespacet &);
2322
exprt pointer_offset(const exprt &pointer);
2423
exprt pointer_object(const exprt &pointer);
2524
exprt object_size(const exprt &pointer);
26-
DEPRECATED(SINCE(2021, 5, 6, "Use is_dynamic_object_exprt instead"))
27-
exprt dynamic_object(const exprt &pointer);
2825
exprt good_pointer(const exprt &pointer);
2926
exprt good_pointer_def(const exprt &pointer, const namespacet &);
3027
exprt null_object(const exprt &pointer);

0 commit comments

Comments
 (0)