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

Stabilize pointer-to-reference cast validity checks #3425

Closed
artemagvanian opened this issue Aug 7, 2024 · 0 comments · Fixed by #3426
Closed

Stabilize pointer-to-reference cast validity checks #3425

artemagvanian opened this issue Aug 7, 2024 · 0 comments · Fixed by #3426
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.

Comments

@artemagvanian
Copy link
Contributor

#3221 introduced additional pointer validity checks when performing pointer-to-reference casts to aid with modular verification.

This led to one harness run on the CI inside s2n-quic timing out, so the checks were introduced behind an unstable flag. The reason for the timeout was that a check was inserted inside a nested loop, which blew up verification time.

One of the pathways for stabilizing the checks is excluding the harness from the CI.
@artemagvanian artemagvanian added the [C] Internal Tracks some internal work. I.e.: Users should not be affected. label Aug 7, 2024
@artemagvanian artemagvanian mentioned this issue Aug 7, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Aug 7, 2024
@artemagvanian
Stabilize pointer-to-reference cast validity checks (#3426)
3fb3a73 
This PR stabilizes pointer-to-reference cast validity checks, so that
they are run by default.

Resolves #3425 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Stabilize pointer-to-reference cast validity checks artemagvanian/kani
1 participant
@artemagvanian