Skip to content

Commit 67dfd8c

Browse files
authored
Update RAPx toolchain to nightly-2026-02-05 (#690)
This pr mainly follows the latest verify-rust-std toolchain update. - Bumped RAPx CI to RAPx 0.7.50 on nightly-2026-02-05. - Slightly refined several contracts related to Challenge 17 to make them more compact and accurate.
1 parent 5210ea4 commit 67dfd8c

4 files changed

Lines changed: 9 additions & 8 deletions

File tree

‎.github/pull_requests.toml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,5 +18,6 @@ members = [
1818
"btj",
1919
"rafaelsamenezes",
2020
"lucasccordeiro",
21-
"dkcumming"
21+
"dkcumming",
22+
"DiuDiu777"
2223
]

‎.github/workflows/rapx.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@ on:
88
branches: [main]
99

1010
env:
11-
RAPX_VERSION: "0.7.38"
12-
TOOLCHAIN: "nightly-2025-11-25"
11+
RAPX_VERSION: "0.7.50"
12+
TOOLCHAIN: "nightly-2026-02-05"
1313

1414
jobs:
1515
verify-slice:

‎library/core/src/slice/mod.rs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -649,7 +649,7 @@ impl<T> [T] {
649649
#[track_caller]
650650
#[rustc_const_unstable(feature = "const_index", issue = "143775")]
651651
#[cfg_attr(rapx, rapx::verify)]
652-
#[cfg_attr(rapx, rapx::requires(InBound(index_access(self, index))))]
652+
#[cfg_attr(rapx, rapx::requires(InBound(self, index)))]
653653
pub const unsafe fn get_unchecked<I>(&self, index: I) -> &I::Output
654654
where
655655
I: [const] SliceIndex<Self>,
@@ -696,7 +696,7 @@ impl<T> [T] {
696696
#[track_caller]
697697
#[rustc_const_unstable(feature = "const_index", issue = "143775")]
698698
#[cfg_attr(rapx, rapx::verify)]
699-
#[cfg_attr(rapx, rapx::requires(InBound(index_access(self, index))))]
699+
#[cfg_attr(rapx, rapx::requires(InBound(self, index)))]
700700
pub const unsafe fn get_unchecked_mut<I>(&mut self, index: I) -> &mut I::Output
701701
where
702702
I: [const] SliceIndex<Self>,
@@ -5261,7 +5261,7 @@ impl<T> [T] {
52615261
#[inline]
52625262
#[track_caller]
52635263
#[cfg_attr(rapx, rapx::verify)]
5264-
#[cfg_attr(rapx, rapx::requires(InBound(index_access(self, indices))))]
5264+
#[cfg_attr(rapx, rapx::requires(InBound(self, indices)))]
52655265
#[cfg_attr(rapx, rapx::requires(NonOverlap(indices)))]
52665266
pub unsafe fn get_disjoint_unchecked_mut<I, const N: usize>(
52675267
&mut self,

‎library/core/src/slice/raw.rs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,7 @@ use crate::{array, ptr, ub_checks};
124124
#[cfg_attr(rapx, rapx::requires(NonNull(data)))]
125125
#[cfg_attr(rapx, rapx::requires(ValidPtr(data, T, len)))]
126126
#[cfg_attr(rapx, rapx::requires(Init(data, T, len)))]
127-
#[cfg_attr(rapx, rapx::requires(Alive(data)))]
127+
#[cfg_attr(rapx, rapx::requires(Alive(data, 'a)))]
128128
#[cfg_attr(rapx, rapx::requires(Alias(data)))]
129129
#[cfg_attr(rapx, rapx::requires(Align(data, T)))]
130130
#[cfg_attr(rapx, rapx::requires(ValidNum(size_of(T) * len <= isize::MAX)))]
@@ -186,7 +186,7 @@ pub const unsafe fn from_raw_parts<'a, T>(data: *const T, len: usize) -> &'a [T]
186186
#[cfg_attr(rapx, rapx::requires(NonNull(data)))]
187187
#[cfg_attr(rapx, rapx::requires(ValidPtr(data, T, len)))]
188188
#[cfg_attr(rapx, rapx::requires(Init(data, T, len)))]
189-
#[cfg_attr(rapx, rapx::requires(Alive(data)))]
189+
#[cfg_attr(rapx, rapx::requires(Alive(data, 'a)))]
190190
#[cfg_attr(rapx, rapx::requires(Alias(data)))]
191191
#[cfg_attr(rapx, rapx::requires(Align(data, T)))]
192192
#[cfg_attr(rapx, rapx::requires(ValidNum(size_of(T) * len <= isize::MAX)))]

0 commit comments

Comments
 (0)