Skip to content

Deprecate dynamic_object pointer predicate #6084

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 6, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions src/util/pointer_predicates.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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));

Expand Down
1 change: 1 addition & 0 deletions src/util/pointer_predicates.h
Original file line number Diff line number Diff line change
Expand Up @@ -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 &);
Expand Down