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

Kani may miss invalid accesses in std #3079

Closed
zhassan-aws opened this issue Mar 14, 2024 · 0 comments · Fixed by #3080
Closed

Kani may miss invalid accesses in std #3079

zhassan-aws opened this issue Mar 14, 2024 · 0 comments · Fixed by #3080
Assignees
@tautschnig @zhassan-aws
Labels
[C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue T-High Priority Tag issues that have high priority

Comments

@zhassan-aws
Copy link
Contributor

The fix to #3061 only applies to code outside of std. We need to extend the fix to std as well, to make sure any invalid accesses in std are captured by Kani.
@zhassan-aws zhassan-aws added [C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue labels Mar 14, 2024
@zhassan-aws zhassan-aws mentioned this issue Mar 14, 2024
Merged
@celinval celinval added the T-High Priority Tag issues that have high priority label Mar 15, 2024
@adpaco-aws adpaco-aws mentioned this issue Mar 22, 2024
Merged
tautschnig pushed a commit that referenced this issue Apr 5, 2024
@zhassan-aws
Ensure storage markers are kept in std code (#3080)
c4f16e9 
This is a follow-up to #3063 that turns off that MIR pass while
compiling `std` as well to ensure any bugs of the same nature in `std`
are captured by Kani.

Resolves #3079
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@tautschnig tautschnig

@zhassan-aws zhassan-aws

Labels
[C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue T-High Priority Tag issues that have high priority
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Ensure storage markers are kept in std code zhassan-aws/kani
3 participants
@tautschnig @celinval @zhassan-aws