Skip to content

Commit 3a6157e

Browse files
btjbtj
committed
Sync the VeriFast proofs
1 parent f7f8c5d commit 3a6157e

4 files changed

Lines changed: 24 additions & 48 deletions

File tree

‎verifast-proofs/alloc/collections/linked_list.rs-negative/original/linked_list.rs‎

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1140,7 +1140,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
11401140
/// Splitting a list into evens and odds, reusing the original list:
11411141
///
11421142
/// ```
1143-
/// #![feature(extract_if)]
11441143
/// use std::collections::LinkedList;
11451144
///
11461145
/// let mut numbers: LinkedList<u32> = LinkedList::new();
@@ -1152,7 +1151,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
11521151
/// assert_eq!(evens.into_iter().collect::<Vec<_>>(), vec![2, 4, 6, 8, 14]);
11531152
/// assert_eq!(odds.into_iter().collect::<Vec<_>>(), vec![1, 3, 5, 9, 11, 13, 15]);
11541153
/// ```
1155-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1154+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
11561155
pub fn extract_if<F>(&mut self, filter: F) -> ExtractIf<'_, T, F, A>
11571156
where
11581157
F: FnMut(&mut T) -> bool,
@@ -1932,24 +1931,22 @@ impl<'a, T, A: Allocator> CursorMut<'a, T, A> {
19321931
}
19331932

19341933
/// An iterator produced by calling `extract_if` on LinkedList.
1935-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1934+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
19361935
#[must_use = "iterators are lazy and do nothing unless consumed"]
19371936
pub struct ExtractIf<
19381937
'a,
19391938
T: 'a,
19401939
F: 'a,
19411940
#[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
1942-
> where
1943-
F: FnMut(&mut T) -> bool,
1944-
{
1941+
> {
19451942
list: &'a mut LinkedList<T, A>,
19461943
it: Option<NonNull<Node<T>>>,
19471944
pred: F,
19481945
idx: usize,
19491946
old_len: usize,
19501947
}
19511948

1952-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1949+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
19531950
impl<T, F, A: Allocator> Iterator for ExtractIf<'_, T, F, A>
19541951
where
19551952
F: FnMut(&mut T) -> bool,
@@ -1978,11 +1975,8 @@ where
19781975
}
19791976
}
19801977

1981-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1982-
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F>
1983-
where
1984-
F: FnMut(&mut T) -> bool,
1985-
{
1978+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
1979+
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F> {
19861980
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
19871981
f.debug_tuple("ExtractIf").field(&self.list).finish()
19881982
}

‎verifast-proofs/alloc/collections/linked_list.rs-negative/verified/linked_list.rs‎

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1305,7 +1305,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
13051305
/// Splitting a list into evens and odds, reusing the original list:
13061306
///
13071307
/// ```
1308-
/// #![feature(extract_if)]
13091308
/// use std::collections::LinkedList;
13101309
///
13111310
/// let mut numbers: LinkedList<u32> = LinkedList::new();
@@ -1317,7 +1316,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
13171316
/// assert_eq!(evens.into_iter().collect::<Vec<_>>(), vec![2, 4, 6, 8, 14]);
13181317
/// assert_eq!(odds.into_iter().collect::<Vec<_>>(), vec![1, 3, 5, 9, 11, 13, 15]);
13191318
/// ```
1320-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1319+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
13211320
pub fn extract_if<F>(&mut self, filter: F) -> ExtractIf<'_, T, F, A>
13221321
where
13231322
F: FnMut(&mut T) -> bool,
@@ -2097,24 +2096,22 @@ impl<'a, T, A: Allocator> CursorMut<'a, T, A> {
20972096
}
20982097

20992098
/// An iterator produced by calling `extract_if` on LinkedList.
2100-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
2099+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
21012100
#[must_use = "iterators are lazy and do nothing unless consumed"]
21022101
pub struct ExtractIf<
21032102
'a,
21042103
T: 'a,
21052104
F: 'a,
21062105
#[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
2107-
> where
2108-
F: FnMut(&mut T) -> bool,
2109-
{
2106+
> {
21102107
list: &'a mut LinkedList<T, A>,
21112108
it: Option<NonNull<Node<T>>>,
21122109
pred: F,
21132110
idx: usize,
21142111
old_len: usize,
21152112
}
21162113

2117-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
2114+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
21182115
impl<T, F, A: Allocator> Iterator for ExtractIf<'_, T, F, A>
21192116
where
21202117
F: FnMut(&mut T) -> bool,
@@ -2143,11 +2140,8 @@ where
21432140
}
21442141
}
21452142

2146-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
2147-
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F>
2148-
where
2149-
F: FnMut(&mut T) -> bool,
2150-
{
2143+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
2144+
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F> {
21512145
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
21522146
f.debug_tuple("ExtractIf").field(&self.list).finish()
21532147
}

‎verifast-proofs/alloc/collections/linked_list.rs/original/linked_list.rs‎

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1140,7 +1140,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
11401140
/// Splitting a list into evens and odds, reusing the original list:
11411141
///
11421142
/// ```
1143-
/// #![feature(extract_if)]
11441143
/// use std::collections::LinkedList;
11451144
///
11461145
/// let mut numbers: LinkedList<u32> = LinkedList::new();
@@ -1152,7 +1151,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
11521151
/// assert_eq!(evens.into_iter().collect::<Vec<_>>(), vec![2, 4, 6, 8, 14]);
11531152
/// assert_eq!(odds.into_iter().collect::<Vec<_>>(), vec![1, 3, 5, 9, 11, 13, 15]);
11541153
/// ```
1155-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1154+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
11561155
pub fn extract_if<F>(&mut self, filter: F) -> ExtractIf<'_, T, F, A>
11571156
where
11581157
F: FnMut(&mut T) -> bool,
@@ -1932,24 +1931,22 @@ impl<'a, T, A: Allocator> CursorMut<'a, T, A> {
19321931
}
19331932

19341933
/// An iterator produced by calling `extract_if` on LinkedList.
1935-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1934+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
19361935
#[must_use = "iterators are lazy and do nothing unless consumed"]
19371936
pub struct ExtractIf<
19381937
'a,
19391938
T: 'a,
19401939
F: 'a,
19411940
#[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
1942-
> where
1943-
F: FnMut(&mut T) -> bool,
1944-
{
1941+
> {
19451942
list: &'a mut LinkedList<T, A>,
19461943
it: Option<NonNull<Node<T>>>,
19471944
pred: F,
19481945
idx: usize,
19491946
old_len: usize,
19501947
}
19511948

1952-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1949+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
19531950
impl<T, F, A: Allocator> Iterator for ExtractIf<'_, T, F, A>
19541951
where
19551952
F: FnMut(&mut T) -> bool,
@@ -1978,11 +1975,8 @@ where
19781975
}
19791976
}
19801977

1981-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1982-
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F>
1983-
where
1984-
F: FnMut(&mut T) -> bool,
1985-
{
1978+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
1979+
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F> {
19861980
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
19871981
f.debug_tuple("ExtractIf").field(&self.list).finish()
19881982
}

‎verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs‎

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1305,7 +1305,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
13051305
/// Splitting a list into evens and odds, reusing the original list:
13061306
///
13071307
/// ```
1308-
/// #![feature(extract_if)]
13091308
/// use std::collections::LinkedList;
13101309
///
13111310
/// let mut numbers: LinkedList<u32> = LinkedList::new();
@@ -1317,7 +1316,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
13171316
/// assert_eq!(evens.into_iter().collect::<Vec<_>>(), vec![2, 4, 6, 8, 14]);
13181317
/// assert_eq!(odds.into_iter().collect::<Vec<_>>(), vec![1, 3, 5, 9, 11, 13, 15]);
13191318
/// ```
1320-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
1319+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
13211320
pub fn extract_if<F>(&mut self, filter: F) -> ExtractIf<'_, T, F, A>
13221321
where
13231322
F: FnMut(&mut T) -> bool,
@@ -2097,24 +2096,22 @@ impl<'a, T, A: Allocator> CursorMut<'a, T, A> {
20972096
}
20982097

20992098
/// An iterator produced by calling `extract_if` on LinkedList.
2100-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
2099+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
21012100
#[must_use = "iterators are lazy and do nothing unless consumed"]
21022101
pub struct ExtractIf<
21032102
'a,
21042103
T: 'a,
21052104
F: 'a,
21062105
#[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
2107-
> where
2108-
F: FnMut(&mut T) -> bool,
2109-
{
2106+
> {
21102107
list: &'a mut LinkedList<T, A>,
21112108
it: Option<NonNull<Node<T>>>,
21122109
pred: F,
21132110
idx: usize,
21142111
old_len: usize,
21152112
}
21162113

2117-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
2114+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
21182115
impl<T, F, A: Allocator> Iterator for ExtractIf<'_, T, F, A>
21192116
where
21202117
F: FnMut(&mut T) -> bool,
@@ -2143,11 +2140,8 @@ where
21432140
}
21442141
}
21452142

2146-
#[unstable(feature = "extract_if", reason = "recently added", issue = "43244")]
2147-
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F>
2148-
where
2149-
F: FnMut(&mut T) -> bool,
2150-
{
2143+
#[stable(feature = "extract_if", since = "CURRENT_RUSTC_VERSION")]
2144+
impl<T: fmt::Debug, F> fmt::Debug for ExtractIf<'_, T, F> {
21512145
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
21522146
f.debug_tuple("ExtractIf").field(&self.list).finish()
21532147
}

0 commit comments

Comments
 (0)