diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 9b8753cdd8e..c2ea726335f 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -4001,7 +4001,6 @@ optionalt expr2ct::convert_function(const exprt &src) {ID_gcc_builtin_va_arg, "gcc_builtin_va_arg"}, {ID_get_may, CPROVER_PREFIX "get_may"}, {ID_get_must, CPROVER_PREFIX "get_must"}, - {ID_good_pointer, "GOOD_POINTER"}, {ID_ieee_float_equal, "IEEE_FLOAT_EQUAL"}, {ID_ieee_float_notequal, "IEEE_FLOAT_NOTEQUAL"}, {ID_infinity, "INFINITY"}, diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 5570a62a194..7a853e8549f 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -16,6 +16,7 @@ Date: September 2021 #include #include #include +#include #include #include #include @@ -85,9 +86,13 @@ exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns) { exprt::operandst validity_checks; - if(expr.id() == ID_dereference) - validity_checks.push_back( - good_pointer_def(to_dereference_expr(expr).pointer(), ns)); + if(auto deref = expr_try_dynamic_cast(expr)) + { + const auto size_of_expr_opt = size_of_expr(expr.type(), ns); + CHECK_RETURN(size_of_expr_opt.has_value()); + + validity_checks.push_back(r_ok_exprt{deref->pointer(), *size_of_expr_opt}); + } for(const auto &op : expr.operands()) validity_checks.push_back(all_dereferences_are_valid(op, ns)); diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 99595940b90..4a9b8a07213 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -62,8 +62,8 @@ class havoc_assigns_targetst : public havoc_if_validt /// /// This function generates a formula: /// -/// good_pointer_def(pexpr_1, ns) && -/// good_pointer_def(pexpr_2, n2) && +/// r_ok_exprt(pexpr_1, sizeof(*pexpr_1)) && +/// r_ok_exprt(pexpr_2, sizeof(*pexpr_1)) && /// ... /// /// over all dereferenced pointer expressions *(pexpr_1), *(pexpr_2), ... diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index e33c96bb0b2..46421875ea2 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -461,7 +461,6 @@ IREP_ID_TWO(C_dynamic, #dynamic) IREP_ID_ONE(pointer_in_range) IREP_ID_ONE(object_size) IREP_ID_ONE(separate) -IREP_ID_ONE(good_pointer) IREP_ID_ONE(live_object) IREP_ID_ONE(writeable_object) IREP_ID_ONE(integer_address) diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index c54aebda615..429fe4b6417 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -56,34 +56,6 @@ exprt dead_object(const exprt &pointer, const namespacet &ns) return same_object(pointer, deallocated_symbol.symbol_expr()); } -exprt good_pointer(const exprt &pointer) -{ - return unary_exprt(ID_good_pointer, pointer, bool_typet()); -} - -exprt good_pointer_def( - const exprt &pointer, - const namespacet &ns) -{ - const pointer_typet &pointer_type = to_pointer_type(pointer.type()); - const typet &dereference_type = pointer_type.base_type(); - - const auto size_of_expr_opt = size_of_expr(dereference_type, ns); - CHECK_RETURN(size_of_expr_opt.has_value()); - - const exprt good_dynamic = not_exprt{deallocated(pointer, ns)}; - - const not_exprt not_null(null_object(pointer)); - - const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}}; - - 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_bounds); -} - exprt null_object(const exprt &pointer) { null_pointer_exprt null_pointer(to_pointer_type(pointer.type())); diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h index 8673f732edb..b909834a344 100644 --- a/src/util/pointer_predicates.h +++ b/src/util/pointer_predicates.h @@ -22,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); -exprt good_pointer(const exprt &pointer); -exprt good_pointer_def(const exprt &pointer, const namespacet &); exprt null_object(const exprt &pointer); exprt integer_address(const exprt &pointer); diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 7a99b9dc340..0b47a7cbf97 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2734,10 +2734,6 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node) { r = simplify_object_size(*object_size); } - else if(expr.id()==ID_good_pointer) - { - r = simplify_good_pointer(to_unary_expr(expr)); - } else if(expr.id()==ID_div) { r = simplify_div(to_div_expr(expr)); diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index b4e4b6b078d..f1ecb47e4a4 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -180,7 +180,6 @@ class simplify_exprt NODISCARD resultt<> simplify_object_size(const object_size_exprt &); NODISCARD resultt<> simplify_is_dynamic_object(const unary_exprt &); NODISCARD resultt<> simplify_is_invalid_pointer(const unary_exprt &); - NODISCARD resultt<> simplify_good_pointer(const unary_exprt &); NODISCARD resultt<> simplify_object(const exprt &); NODISCARD resultt<> simplify_unary_minus(const unary_minus_exprt &); NODISCARD resultt<> simplify_unary_plus(const unary_plus_exprt &); diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 797e2d5bdf6..40c9848eef4 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -692,13 +692,3 @@ simplify_exprt::simplify_object_size(const object_size_exprt &expr) else return std::move(new_expr); } - -simplify_exprt::resultt<> -simplify_exprt::simplify_good_pointer(const unary_exprt &expr) -{ - // we expand the definition - exprt def = good_pointer_def(expr.op(), ns); - - // recursive call - return changed(simplify_rec(def)); -}