Skip to content

Conversation

@zhassan-aws
Copy link
Contributor

@zhassan-aws zhassan-aws commented Apr 14, 2025

Keeping it as a draft till we figure out what's causing tests/kani/FunctionContracts/modify_slice_elem.rs to fail.

Resolves #4009

Relevant upstream changes:

  • rust-lang/rust@9eca59a: Removes the Option wrapper from DefPathData::TypeNs.
  • rust-lang/rust@50d0ce1: The changes made to the ptr module cause one of the failed unsupported checks to disappear (in tests/expected/uninit/intrinsics/intrinsics.rs)
  • (Pointed out by @tautschnig) The combination of rust-lang/rust@78e9621390 and rust-lang/rust@aadfd810f6: these cause us to now assign a non-deterministic value when using contracts causing a spurious failure in tests/kani/FunctionContracts/modify_slice_elem.rs. We've made this a fixme test till we figure out a fix.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Apr 14, 2025
@zhassan-aws zhassan-aws force-pushed the toolchain-2025-04-14 branch from e2e7aad to 9574a33 Compare April 14, 2025 23:53
@zhassan-aws zhassan-aws marked this pull request as ready for review April 17, 2025 23:46
@zhassan-aws zhassan-aws requested a review from a team as a code owner April 17, 2025 23:46
@zhassan-aws
Copy link
Contributor Author

Based on the investigation in #4009, I turned the failing test into a fixme test and created a tracking issue (#4029). This is now ready for review.

Copy link
Contributor

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! Can you update the PR descriptions with the culprit PRs before merging?

@zhassan-aws zhassan-aws added this pull request to the merge queue Apr 18, 2025
Merged via the queue into model-checking:main with commit a61a52b Apr 18, 2025
25 of 26 checks passed
@zhassan-aws zhassan-aws deleted the toolchain-2025-04-14 branch April 18, 2025 17:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Toolchain upgrade to nightly-2025-04-08 failed

2 participants