Merge pull request #6084 from tautschnig/deprecate-dynamic_object

Deprecate dynamic_object pointer predicate

Author: tautschnig

src/util/pointer_predicates.cpp

@@ -91,8 +91,7 @@ exprt good_pointer_def(
   const auto size_of_expr_opt = size_of_expr(dereference_type, ns);
   CHECK_RETURN(size_of_expr_opt.has_value());
 
-  const or_exprt good_dynamic(
-    not_exprt(dynamic_object(pointer)), not_exprt(deallocated(pointer, ns)));
+  const exprt good_dynamic = not_exprt{deallocated(pointer, ns)};
 
   const not_exprt not_null(null_pointer(pointer));
 

src/util/pointer_predicates.h

@@ -26,6 +26,7 @@ exprt pointer_offset(const exprt &pointer);
 exprt pointer_object(const exprt &pointer);
 exprt malloc_object(const exprt &pointer, const namespacet &);
 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 &);