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.

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

CStr Invariant proofs for bytes, as_ptr, to_str #192

Conversation

rajathkotyal
Copy link

Towards #150

Verifies that the CStr safety invariant holds after calling :

bytes core::ffi::c_str
to_str core::ffi::c_str
as_ptr core::ffi::c_str

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@rajathkotyal rajathkotyal requested a review from a team as a code owner November 28, 2024 06:09
@rajathkotyal rajathkotyal changed the title C 0013 rajathm bytes as ptr to str CStr Invariant proofs for bytes, as_ptr, to_str Nov 28, 2024
library/core/src/ffi/c_str.rs Outdated Show resolved Hide resolved
@tautschnig
Copy link
Member

@rajathkotyal Could you please resolve the conflicts that just came up?

Copy link

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hi @rajathkotyal, is it possible to use arbitrary_cstr function in these harnesses?

@rajathkotyal
Copy link
Author

Sure, updated code @celinval

Copy link

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@rajathkotyal
Copy link
Author

Thanks @celinval , can we get a workflow approval for this PR?

@carolynzech carolynzech enabled auto-merge (squash) December 4, 2024 14:50
@carolynzech carolynzech merged commit d9780d6 into model-checking:main Dec 4, 2024
9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants