Add a new method to check whether a pointer points to a valid location

[celinval]

I would like to be able to instrument my code to check that one or more pointers can be safely dereferenced, i.e., that the pointer points to an allocated object.

From the discussion in #8199, we concluded that this cannot be achieved by using __CPROVER_r_ok, since its behavior isn't well defined for invalid pointers.

Ideally, we would have an API similar to __CPROVER_r_ok that returns false when the pointer argument isn't dereferenceable.

In the meantime, I was wondering what is the proper way of asserting that a pointer is valid.

Thanks!

[kroening]

The discussion about __CPROVER_r_ok is wrong. You can of course assert that __CPROVER_r_ok holds. CBMC does that automatically when you dereference a pointer, and --pointer-check is on.
I suspect that the reason why someone claimed at some point that it's undefined for invalid pointers was a misunderstanding owing to the fact that you cannot use __CPROVER_r_ok in assumptions.

[celinval]

The discussion about __CPROVER_r_ok is wrong. You can of course assert that __CPROVER_r_ok holds. CBMC does that automatically when you dereference a pointer, and --pointer-check is on. I suspect that the reason why someone claimed at some point that it's undefined for invalid pointers was a misunderstanding owing to the fact that you cannot use __CPROVER_r_ok in assumptions.

Thank you for the update. I'll reopen #8199 so the documentation can be updated.

I'll leave this issue open since we still require an API that always returns false for invalid pointers, which would allow us to use it in different contexts.