Merge pull request #6081 from tautschnig/deprecate-dynamic_size

Deprecate unnecessary dynamic_size pointer predicate

Author: kroening

src/util/pointer_predicates.cpp

@@ -91,34 +91,18 @@ 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_tmp1(
-    not_exprt(malloc_object(pointer, ns)),
-    and_exprt(
-      not_exprt(dynamic_object_lower_bound(pointer, nil_exprt())),
-      not_exprt(
-        dynamic_object_upper_bound(pointer, ns, size_of_expr_opt.value()))));
-
-  const and_exprt good_dynamic_tmp2(
-    not_exprt(deallocated(pointer, ns)), good_dynamic_tmp1);
-
   const or_exprt good_dynamic(
-    not_exprt(dynamic_object(pointer)), good_dynamic_tmp2);
+    not_exprt(dynamic_object(pointer)), not_exprt(deallocated(pointer, ns)));
 
   const not_exprt not_null(null_pointer(pointer));
 
   const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}};
 
-  const or_exprt bad_other(
-    object_lower_bound(pointer, nil_exprt()),
-    object_upper_bound(pointer, size_of_expr_opt.value()));
-
-  const or_exprt good_other(dynamic_object(pointer), not_exprt(bad_other));
+  const and_exprt good_bounds{
+    not_exprt{object_lower_bound(pointer, nil_exprt())},
+    not_exprt{object_upper_bound(pointer, size_of_expr_opt.value())}};
 
-  return and_exprt(
-    not_null,
-    not_invalid,
-    good_dynamic,
-    good_other);
+  return and_exprt(not_null, not_invalid, good_dynamic, good_bounds);
 }
 
 exprt null_object(const exprt &pointer)

src/util/pointer_predicates.h

@@ -12,13 +12,15 @@ 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::"
 
 exprt same_object(const exprt &p1, const exprt &p2);
 exprt deallocated(const exprt &pointer, const namespacet &);
 exprt dead_object(const exprt &pointer, const namespacet &);
+DEPRECATED(SINCE(2021, 5, 6, "Use object_size instead"))
 exprt dynamic_size(const namespacet &);
 exprt pointer_offset(const exprt &pointer);
 exprt pointer_object(const exprt &pointer);
@@ -30,9 +32,11 @@ exprt good_pointer_def(const exprt &pointer, const namespacet &);
 exprt null_object(const exprt &pointer);
 exprt null_pointer(const exprt &pointer);
 exprt integer_address(const exprt &pointer);
+DEPRECATED(SINCE(2021, 5, 6, "Use object_lower_bound instead"))
 exprt dynamic_object_lower_bound(
   const exprt &pointer,
   const exprt &offset);
+DEPRECATED(SINCE(2021, 5, 6, "Use object_upper_bound instead"))
 exprt dynamic_object_upper_bound(
   const exprt &pointer,
   const namespacet &,