-
Notifications
You must be signed in to change notification settings - Fork 97
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
Upgrade toolchain to nightly-2024-04-15 #3144
Conversation
- rust-lang/rust#120131: Add support to `Pat` pattern type - rust-lang/rust#122935: Rename CastKind::PointerWithExposedProvenance - rust-lang/rust#123097: Adapt to changes to local_def_path_hash_to_def_id
The return value is in fact an enumeration, not an integer
Note to self: Add a test to Pat to ensure we capture invalid valid generated during a transmute. |
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.
For my own learning: the changes in 1abfa0f ("Fix BinOp implementation") seem much bigger than what I initially had for the Cmp operator. Could you please explain a bit?
I added a comment to the code, which explains why this is slightly more complex. The result of a comparison is not an integer, but an enumeration. So Kani would crash with the previous implementation when it would try to assign the comparison expression due to mismatched type. Part of the logic I added is to guarantee that the transmute is safe, but it is not really necessary. But I check that the enumeration layout matches what we expect, which is an i8 that goes from -1 to 1. |
I'm merging this PR despite the issue with the benchmark job, since it is blocked due to a bug in the benchcomp tool itself. It is failing to generate the comparison tables since the base commit is currently broken due to #3138 |
Related changes: - rust-lang/rust#118310: Add `Ord::cmp` for primitives as a `BinOp` in MIR - rust-lang/rust#120131: Add support to `Pat` pattern type - rust-lang/rust#122935: Rename CastKind::PointerWithExposedProvenance - rust-lang/rust#123097: Adapt to changes to local_def_path_hash_to_def_id Resolves model-checking#3130, model-checking#3142
Related changes: - rust-lang/rust#118310: Add `Ord::cmp` for primitives as a `BinOp` in MIR - rust-lang/rust#120131: Add support to `Pat` pattern type - rust-lang/rust#122935: Rename CastKind::PointerWithExposedProvenance - rust-lang/rust#123097: Adapt to changes to local_def_path_hash_to_def_id Resolves model-checking#3130, model-checking#3142
Related changes:
Ord::cmp
for primitives as aBinOp
in MIR rust-lang/rust#118310:Add
Ord::cmp
for primitives as aBinOp
in MIRAdd support to
Pat
pattern typeRename CastKind::PointerWithExposedProvenance
dyn Debug
trait object instead of a closure rust-lang/rust#123097:Adapt to changes to local_def_path_hash_to_def_id
Resolves #3130, #3142
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.