Skip to content
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.

Sign up for GitHub

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

Jump to bottom

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

Open
celinval opened this issue Feb 22, 2024 · 2 comments · May be fixed by #8472
Open

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

celinval opened this issue Feb 22, 2024 · 2 comments · May be fixed by #8472
Labels
aws Bugs or features of importance to AWS CBMC users feature request pending merge

Comments

@celinval
Copy link
Collaborator

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!
@celinval celinval added aws Bugs or features of importance to AWS CBMC users feature request labels Feb 22, 2024
@celinval celinval mentioned this issue Feb 22, 2024
Open
@kroening
Copy link
Member

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 celinval mentioned this issue Feb 22, 2024
Closed
@celinval
Copy link
Collaborator Author

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.

tautschnig added a commit to tautschnig/cbmc that referenced this issue Sep 25, 2024
@tautschnig
Reword documentation of __CPROVER_{r,w,rw}_ok
cfc3277 
It is safe to use these primitives for asserting validity of pointers.

Fixes: diffblue#8217, diffblue#8199
@tautschnig tautschnig linked a pull request Sep 25, 2024 that will close this issue
Open
3 tasks
@tautschnig tautschnig removed their assignment Sep 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
aws Bugs or features of importance to AWS CBMC users feature request pending merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Reword documentation of __CPROVER_{r,w,rw}_ok tautschnig/cbmc
3 participants
@tautschnig @kroening @celinval