Add Flux specifications to path/bstr/hash/time #438
Conversation
library/core/src/num/niche_types.rs
Outdated
| @@ -49,12 +53,14 @@ macro_rules! define_valid_range_type { | |||
| /// Immediate language UB if `val == 0`, as it violates the validity | |||
| /// invariant of this type. | |||
| #[inline] | |||
| #[cfg_attr(flux, flux::spec(fn (val: $int{ $low <= cast(val) && cast(val) <= $high }) -> Self[{val:cast(val)}]))] // NOTE: `val == 0` comments are stale(?) | |||
There was a problem hiding this comment.
I'd agree that 0 is not relevant here (anymore?) - would you mind creating an upstream PR that proposes to fix this?
There was a problem hiding this comment.
Sure thing, @nilehmann will you be able to do this?
nilehmann
force-pushed
the
verify-time-rs
branch
from
dc3829c to
242f5f7
Compare
| @@ -508,6 +509,7 @@ impl AsciiChar { | |||
| /// when writing code using this method, since the implementation doesn't | |||
| /// need something really specific, not to make those other arguments do | |||
| /// something useful. It might be tightened before stabilization.) | |||
| #[cfg_attr(flux, flux::spec(fn(d: u8{d < 10}) -> Self))] | |||
There was a problem hiding this comment.
The safety comment doesn't match the UB assertion inside the function, so I wasn't sure which one to choose. If the intention is to keep the more relaxed version, then maybe we should change the UB assertion upstream.
There was a problem hiding this comment.
Yes I picked 10 because that’s what the assertion inside the function checked..
There was a problem hiding this comment.
I think we should get something changed upstream. It doesn't seem right to have an assert_unsafe_precondition with d < 10 here as there isn't really anything unsafe up until 63 (could be a debug_assert instead). If they, however, deem it unsafe between 10 and 63 because of some other piece of code then the comment should be changed.
There was a problem hiding this comment.
I think they just yoloed it rust-lang#129374
There was a problem hiding this comment.
Thank you for digging deeper! So I'd say pick whichever you prefer at this point, but please include a comment noting the disparity (and possibly linking to that PR).
There was a problem hiding this comment.
@nilehmann FWIW the code checks if we change it to d <= 64 (as in the unchecked_add is fine...)
nilehmann
force-pushed
the
verify-time-rs
branch
from
4c8506b to
87c72a3
Compare
nilehmann
force-pushed
the
verify-time-rs
branch
from
87c72a3 to
a6a7882
Compare
This PR adds flux specifications for checking the following modules in core
In particular, it verifies that
Nanosecondsis correctly used with values within the range.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.