Merge pull request #6672 from tautschnig/cleanup/remove-deprecated-dynamic_object

Remove deprecated dynamic_object pointer predicate

Author: tautschnig

src/pointer-analysis/value_set_dereference.cpp

@@ -480,7 +480,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
   {
     // constraint that it actually is a dynamic object
     // this is also our guard
-    result.pointer_guard = dynamic_object(pointer_expr);
+    result.pointer_guard = is_dynamic_object_exprt(pointer_expr);
 
     // can't remove here, turn into *p
     result.value = dereference_exprt{pointer_expr};

src/util/pointer_predicates.cpp

@@ -56,13 +56,6 @@ exprt dead_object(const exprt &pointer, const namespacet &ns)
   return same_object(pointer, deallocated_symbol.symbol_expr());
 }
 
-exprt dynamic_object(const exprt &pointer)
-{
-  exprt dynamic_expr(ID_is_dynamic_object, bool_typet());
-  dynamic_expr.copy_to_operands(pointer);
-  return dynamic_expr;
-}
-
 exprt good_pointer(const exprt &pointer)
 {
   return unary_exprt(ID_good_pointer, pointer, bool_typet());

src/util/pointer_predicates.h

@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_POINTER_PREDICATES_H
 #define CPROVER_UTIL_POINTER_PREDICATES_H
 
-#include "deprecate.h"
 #include "std_expr.h"
 
 #define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
@@ -23,8 +22,6 @@ exprt dead_object(const exprt &pointer, const namespacet &);
 exprt pointer_offset(const exprt &pointer);
 exprt pointer_object(const exprt &pointer);
 exprt object_size(const exprt &pointer);
-DEPRECATED(SINCE(2021, 5, 6, "Use is_dynamic_object_exprt instead"))
-exprt dynamic_object(const exprt &pointer);
 exprt good_pointer(const exprt &pointer);
 exprt good_pointer_def(const exprt &pointer, const namespacet &);
 exprt null_object(const exprt &pointer);