Skip to content

Commit c72de4d

Browse files
author
gitbot
committed
Update VeriFast proofs
1 parent a1f0e0d commit c72de4d

File tree

4 files changed

+8
-148
lines changed

4 files changed

+8
-148
lines changed

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

Lines changed: 2 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1031,7 +1031,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
10311031

10321032
/// Retains only the elements specified by the predicate.
10331033
///
1034-
/// In other words, remove all elements `e` for which `f(&e)` returns false.
1034+
/// In other words, remove all elements `e` for which `f(&mut e)` returns false.
10351035
/// This method operates in place, visiting each element exactly once in the
10361036
/// original order, and preserves the order of the retained elements.
10371037
///
@@ -1047,7 +1047,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
10471047
/// d.push_front(2);
10481048
/// d.push_front(3);
10491049
///
1050-
/// d.retain(|&x| x % 2 == 0);
1050+
/// d.retain(|&mut x| x % 2 == 0);
10511051
///
10521052
/// assert_eq!(d.pop_front(), Some(2));
10531053
/// assert_eq!(d.pop_front(), None);
@@ -1074,41 +1074,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
10741074
/// ```
10751075
#[unstable(feature = "linked_list_retain", issue = "114135")]
10761076
pub fn retain<F>(&mut self, mut f: F)
1077-
where
1078-
F: FnMut(&T) -> bool,
1079-
{
1080-
self.retain_mut(|elem| f(elem));
1081-
}
1082-
1083-
/// Retains only the elements specified by the predicate.
1084-
///
1085-
/// In other words, remove all elements `e` for which `f(&mut e)` returns false.
1086-
/// This method operates in place, visiting each element exactly once in the
1087-
/// original order, and preserves the order of the retained elements.
1088-
///
1089-
/// # Examples
1090-
///
1091-
/// ```
1092-
/// #![feature(linked_list_retain)]
1093-
/// use std::collections::LinkedList;
1094-
///
1095-
/// let mut d = LinkedList::new();
1096-
///
1097-
/// d.push_front(1);
1098-
/// d.push_front(2);
1099-
/// d.push_front(3);
1100-
///
1101-
/// d.retain_mut(|x| if *x % 2 == 0 {
1102-
/// *x += 1;
1103-
/// true
1104-
/// } else {
1105-
/// false
1106-
/// });
1107-
/// assert_eq!(d.pop_front(), Some(3));
1108-
/// assert_eq!(d.pop_front(), None);
1109-
/// ```
1110-
#[unstable(feature = "linked_list_retain", issue = "114135")]
1111-
pub fn retain_mut<F>(&mut self, mut f: F)
11121077
where
11131078
F: FnMut(&mut T) -> bool,
11141079
{

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

Lines changed: 2 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1196,7 +1196,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
11961196

11971197
/// Retains only the elements specified by the predicate.
11981198
///
1199-
/// In other words, remove all elements `e` for which `f(&e)` returns false.
1199+
/// In other words, remove all elements `e` for which `f(&mut e)` returns false.
12001200
/// This method operates in place, visiting each element exactly once in the
12011201
/// original order, and preserves the order of the retained elements.
12021202
///
@@ -1212,7 +1212,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
12121212
/// d.push_front(2);
12131213
/// d.push_front(3);
12141214
///
1215-
/// d.retain(|&x| x % 2 == 0);
1215+
/// d.retain(|&mut x| x % 2 == 0);
12161216
///
12171217
/// assert_eq!(d.pop_front(), Some(2));
12181218
/// assert_eq!(d.pop_front(), None);
@@ -1239,41 +1239,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
12391239
/// ```
12401240
#[unstable(feature = "linked_list_retain", issue = "114135")]
12411241
pub fn retain<F>(&mut self, mut f: F)
1242-
where
1243-
F: FnMut(&T) -> bool,
1244-
{
1245-
self.retain_mut(|elem| f(elem));
1246-
}
1247-
1248-
/// Retains only the elements specified by the predicate.
1249-
///
1250-
/// In other words, remove all elements `e` for which `f(&mut e)` returns false.
1251-
/// This method operates in place, visiting each element exactly once in the
1252-
/// original order, and preserves the order of the retained elements.
1253-
///
1254-
/// # Examples
1255-
///
1256-
/// ```
1257-
/// #![feature(linked_list_retain)]
1258-
/// use std::collections::LinkedList;
1259-
///
1260-
/// let mut d = LinkedList::new();
1261-
///
1262-
/// d.push_front(1);
1263-
/// d.push_front(2);
1264-
/// d.push_front(3);
1265-
///
1266-
/// d.retain_mut(|x| if *x % 2 == 0 {
1267-
/// *x += 1;
1268-
/// true
1269-
/// } else {
1270-
/// false
1271-
/// });
1272-
/// assert_eq!(d.pop_front(), Some(3));
1273-
/// assert_eq!(d.pop_front(), None);
1274-
/// ```
1275-
#[unstable(feature = "linked_list_retain", issue = "114135")]
1276-
pub fn retain_mut<F>(&mut self, mut f: F)
12771242
where
12781243
F: FnMut(&mut T) -> bool,
12791244
{

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

Lines changed: 2 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1031,7 +1031,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
10311031

10321032
/// Retains only the elements specified by the predicate.
10331033
///
1034-
/// In other words, remove all elements `e` for which `f(&e)` returns false.
1034+
/// In other words, remove all elements `e` for which `f(&mut e)` returns false.
10351035
/// This method operates in place, visiting each element exactly once in the
10361036
/// original order, and preserves the order of the retained elements.
10371037
///
@@ -1047,7 +1047,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
10471047
/// d.push_front(2);
10481048
/// d.push_front(3);
10491049
///
1050-
/// d.retain(|&x| x % 2 == 0);
1050+
/// d.retain(|&mut x| x % 2 == 0);
10511051
///
10521052
/// assert_eq!(d.pop_front(), Some(2));
10531053
/// assert_eq!(d.pop_front(), None);
@@ -1074,41 +1074,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
10741074
/// ```
10751075
#[unstable(feature = "linked_list_retain", issue = "114135")]
10761076
pub fn retain<F>(&mut self, mut f: F)
1077-
where
1078-
F: FnMut(&T) -> bool,
1079-
{
1080-
self.retain_mut(|elem| f(elem));
1081-
}
1082-
1083-
/// Retains only the elements specified by the predicate.
1084-
///
1085-
/// In other words, remove all elements `e` for which `f(&mut e)` returns false.
1086-
/// This method operates in place, visiting each element exactly once in the
1087-
/// original order, and preserves the order of the retained elements.
1088-
///
1089-
/// # Examples
1090-
///
1091-
/// ```
1092-
/// #![feature(linked_list_retain)]
1093-
/// use std::collections::LinkedList;
1094-
///
1095-
/// let mut d = LinkedList::new();
1096-
///
1097-
/// d.push_front(1);
1098-
/// d.push_front(2);
1099-
/// d.push_front(3);
1100-
///
1101-
/// d.retain_mut(|x| if *x % 2 == 0 {
1102-
/// *x += 1;
1103-
/// true
1104-
/// } else {
1105-
/// false
1106-
/// });
1107-
/// assert_eq!(d.pop_front(), Some(3));
1108-
/// assert_eq!(d.pop_front(), None);
1109-
/// ```
1110-
#[unstable(feature = "linked_list_retain", issue = "114135")]
1111-
pub fn retain_mut<F>(&mut self, mut f: F)
11121077
where
11131078
F: FnMut(&mut T) -> bool,
11141079
{

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

Lines changed: 2 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1196,7 +1196,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
11961196

11971197
/// Retains only the elements specified by the predicate.
11981198
///
1199-
/// In other words, remove all elements `e` for which `f(&e)` returns false.
1199+
/// In other words, remove all elements `e` for which `f(&mut e)` returns false.
12001200
/// This method operates in place, visiting each element exactly once in the
12011201
/// original order, and preserves the order of the retained elements.
12021202
///
@@ -1212,7 +1212,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
12121212
/// d.push_front(2);
12131213
/// d.push_front(3);
12141214
///
1215-
/// d.retain(|&x| x % 2 == 0);
1215+
/// d.retain(|&mut x| x % 2 == 0);
12161216
///
12171217
/// assert_eq!(d.pop_front(), Some(2));
12181218
/// assert_eq!(d.pop_front(), None);
@@ -1239,41 +1239,6 @@ impl<T, A: Allocator> LinkedList<T, A> {
12391239
/// ```
12401240
#[unstable(feature = "linked_list_retain", issue = "114135")]
12411241
pub fn retain<F>(&mut self, mut f: F)
1242-
where
1243-
F: FnMut(&T) -> bool,
1244-
{
1245-
self.retain_mut(|elem| f(elem));
1246-
}
1247-
1248-
/// Retains only the elements specified by the predicate.
1249-
///
1250-
/// In other words, remove all elements `e` for which `f(&mut e)` returns false.
1251-
/// This method operates in place, visiting each element exactly once in the
1252-
/// original order, and preserves the order of the retained elements.
1253-
///
1254-
/// # Examples
1255-
///
1256-
/// ```
1257-
/// #![feature(linked_list_retain)]
1258-
/// use std::collections::LinkedList;
1259-
///
1260-
/// let mut d = LinkedList::new();
1261-
///
1262-
/// d.push_front(1);
1263-
/// d.push_front(2);
1264-
/// d.push_front(3);
1265-
///
1266-
/// d.retain_mut(|x| if *x % 2 == 0 {
1267-
/// *x += 1;
1268-
/// true
1269-
/// } else {
1270-
/// false
1271-
/// });
1272-
/// assert_eq!(d.pop_front(), Some(3));
1273-
/// assert_eq!(d.pop_front(), None);
1274-
/// ```
1275-
#[unstable(feature = "linked_list_retain", issue = "114135")]
1276-
pub fn retain_mut<F>(&mut self, mut f: F)
12771242
where
12781243
F: FnMut(&mut T) -> bool,
12791244
{

0 commit comments

Comments
 (0)