-
Notifications
You must be signed in to change notification settings - Fork 28
Add extern specs for all core functions used by ring buffer
#1377
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
Add extern specs for all core functions used by ring buffer
#1377
Conversation
core functions used by ring buffer
…gbuffer-extern-specs
… slice module with no_panic split_at function
enjhnsn2
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Mostly looks good. Specs appear to be sound, but are currently trusted, but it would be good to at least attempt to verify them at some point.
| v[0] | ||
| } | ||
|
|
||
| #[cfg_attr(flux, flux::no_panic)] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
why is this not just #[flux::no_panic]?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@nilehmann deferring to you for a smarter explanation. From what I remember, this has to do with Rust's mechanism for attaching attributes to modules? There's something about #[no_panic] becoming a "macro within a macro" which causes issues when showing up as a module annotation?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Since this is a test, this is actually not needed, because we never run rustc directly on tests. When using this for real, you can't write flux::no_panic directly because during normal compilation, rustc will complain about flux::no_panic not existing.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
wait, but you can do flux_rs::no_panic, correct? Isn't flux_rs the standard way to invoke preconditions/postconditions?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes and no. For this particular example, flux_rs::no_panic would work, but it won't work for file module declaration (the common version of declaring modules), i.e., the following doesn't work.
#[flux_rs::no_panic]
mod my_module;
| @@ -0,0 +1,22 @@ | |||
| #[cfg_attr(flux, flux::no_panic)] | |||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
echo above comment about this being #[flux::no_panic]
| } | ||
|
|
||
|
|
||
| #[cfg_attr(flux, flux::no_panic)] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
#[flux::no_panic]
|
@enjhnsn2 @nilehmann are we good to punt the conversation re: |
That part is already merged so I don't know why we were discussing it at all here 😅 |
|
OK, marking this ready for review then. I think the |
|
@ninehusky LGTM. Can you rebase and push to verify CI is green after #1382 |
|
@nilehmann done! |
Adds
no_panicspecs for the following functions: