Skip to content

Commit 92c3f66

Browse files
author
gitbot
committed
Update VeriFast proofs
1 parent a5a67d1 commit 92c3f66

File tree

4 files changed

+200
-16
lines changed

4 files changed

+200
-16
lines changed

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

Lines changed: 50 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -825,7 +825,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
825825
unsafe { self.tail.as_mut().map(|node| &mut node.as_mut().element) }
826826
}
827827

828-
/// Adds an element first in the list.
828+
/// Adds an element to the front of the list.
829829
///
830830
/// This operation should compute in *O*(1) time.
831831
///
@@ -844,11 +844,34 @@ impl<T, A: Allocator> LinkedList<T, A> {
844844
/// ```
845845
#[stable(feature = "rust1", since = "1.0.0")]
846846
pub fn push_front(&mut self, elt: T) {
847+
let _ = self.push_front_mut(elt);
848+
}
849+
850+
/// Adds an element to the front of the list, returning a reference to it.
851+
///
852+
/// This operation should compute in *O*(1) time.
853+
///
854+
/// # Examples
855+
///
856+
/// ```
857+
/// #![feature(push_mut)]
858+
/// use std::collections::LinkedList;
859+
///
860+
/// let mut dl = LinkedList::from([1, 2, 3]);
861+
///
862+
/// let ptr = dl.push_front_mut(2);
863+
/// *ptr += 4;
864+
/// assert_eq!(dl.front().unwrap(), &6);
865+
/// ```
866+
#[unstable(feature = "push_mut", issue = "135974")]
867+
#[must_use = "if you don't need a reference to the value, use `LinkedList::push_front` instead"]
868+
pub fn push_front_mut(&mut self, elt: T) -> &mut T {
847869
let node = Box::new_in(Node::new(elt), &self.alloc);
848-
let node_ptr = NonNull::from(Box::leak(node));
870+
let mut node_ptr = NonNull::from(Box::leak(node));
849871
// SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked
850872
unsafe {
851873
self.push_front_node(node_ptr);
874+
&mut node_ptr.as_mut().element
852875
}
853876
}
854877

@@ -876,7 +899,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
876899
self.pop_front_node().map(Node::into_element)
877900
}
878901

879-
/// Appends an element to the back of a list.
902+
/// Adds an element to the back of the list.
880903
///
881904
/// This operation should compute in *O*(1) time.
882905
///
@@ -893,11 +916,34 @@ impl<T, A: Allocator> LinkedList<T, A> {
893916
#[stable(feature = "rust1", since = "1.0.0")]
894917
#[rustc_confusables("push", "append")]
895918
pub fn push_back(&mut self, elt: T) {
919+
let _ = self.push_back_mut(elt);
920+
}
921+
922+
/// Adds an element to the back of the list, returning a reference to it.
923+
///
924+
/// This operation should compute in *O*(1) time.
925+
///
926+
/// # Examples
927+
///
928+
/// ```
929+
/// #![feature(push_mut)]
930+
/// use std::collections::LinkedList;
931+
///
932+
/// let mut dl = LinkedList::from([1, 2, 3]);
933+
///
934+
/// let ptr = dl.push_back_mut(2);
935+
/// *ptr += 4;
936+
/// assert_eq!(dl.back().unwrap(), &6);
937+
/// ```
938+
#[unstable(feature = "push_mut", issue = "135974")]
939+
#[must_use = "if you don't need a reference to the value, use `LinkedList::push_back` instead"]
940+
pub fn push_back_mut(&mut self, elt: T) -> &mut T {
896941
let node = Box::new_in(Node::new(elt), &self.alloc);
897-
let node_ptr = NonNull::from(Box::leak(node));
942+
let mut node_ptr = NonNull::from(Box::leak(node));
898943
// SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked
899944
unsafe {
900945
self.push_back_node(node_ptr);
946+
&mut node_ptr.as_mut().element
901947
}
902948
}
903949

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

Lines changed: 50 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -990,7 +990,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
990990
unsafe { self.tail.as_mut().map(|node| &mut node.as_mut().element) }
991991
}
992992

993-
/// Adds an element first in the list.
993+
/// Adds an element to the front of the list.
994994
///
995995
/// This operation should compute in *O*(1) time.
996996
///
@@ -1009,11 +1009,34 @@ impl<T, A: Allocator> LinkedList<T, A> {
10091009
/// ```
10101010
#[stable(feature = "rust1", since = "1.0.0")]
10111011
pub fn push_front(&mut self, elt: T) {
1012+
let _ = self.push_front_mut(elt);
1013+
}
1014+
1015+
/// Adds an element to the front of the list, returning a reference to it.
1016+
///
1017+
/// This operation should compute in *O*(1) time.
1018+
///
1019+
/// # Examples
1020+
///
1021+
/// ```
1022+
/// #![feature(push_mut)]
1023+
/// use std::collections::LinkedList;
1024+
///
1025+
/// let mut dl = LinkedList::from([1, 2, 3]);
1026+
///
1027+
/// let ptr = dl.push_front_mut(2);
1028+
/// *ptr += 4;
1029+
/// assert_eq!(dl.front().unwrap(), &6);
1030+
/// ```
1031+
#[unstable(feature = "push_mut", issue = "135974")]
1032+
#[must_use = "if you don't need a reference to the value, use `LinkedList::push_front` instead"]
1033+
pub fn push_front_mut(&mut self, elt: T) -> &mut T {
10121034
let node = Box::new_in(Node::new(elt), &self.alloc);
1013-
let node_ptr = NonNull::from(Box::leak(node));
1035+
let mut node_ptr = NonNull::from(Box::leak(node));
10141036
// SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked
10151037
unsafe {
10161038
self.push_front_node(node_ptr);
1039+
&mut node_ptr.as_mut().element
10171040
}
10181041
}
10191042

@@ -1041,7 +1064,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
10411064
self.pop_front_node().map(Node::into_element)
10421065
}
10431066

1044-
/// Appends an element to the back of a list.
1067+
/// Adds an element to the back of the list.
10451068
///
10461069
/// This operation should compute in *O*(1) time.
10471070
///
@@ -1058,11 +1081,34 @@ impl<T, A: Allocator> LinkedList<T, A> {
10581081
#[stable(feature = "rust1", since = "1.0.0")]
10591082
#[rustc_confusables("push", "append")]
10601083
pub fn push_back(&mut self, elt: T) {
1084+
let _ = self.push_back_mut(elt);
1085+
}
1086+
1087+
/// Adds an element to the back of the list, returning a reference to it.
1088+
///
1089+
/// This operation should compute in *O*(1) time.
1090+
///
1091+
/// # Examples
1092+
///
1093+
/// ```
1094+
/// #![feature(push_mut)]
1095+
/// use std::collections::LinkedList;
1096+
///
1097+
/// let mut dl = LinkedList::from([1, 2, 3]);
1098+
///
1099+
/// let ptr = dl.push_back_mut(2);
1100+
/// *ptr += 4;
1101+
/// assert_eq!(dl.back().unwrap(), &6);
1102+
/// ```
1103+
#[unstable(feature = "push_mut", issue = "135974")]
1104+
#[must_use = "if you don't need a reference to the value, use `LinkedList::push_back` instead"]
1105+
pub fn push_back_mut(&mut self, elt: T) -> &mut T {
10611106
let node = Box::new_in(Node::new(elt), &self.alloc);
1062-
let node_ptr = NonNull::from(Box::leak(node));
1107+
let mut node_ptr = NonNull::from(Box::leak(node));
10631108
// SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked
10641109
unsafe {
10651110
self.push_back_node(node_ptr);
1111+
&mut node_ptr.as_mut().element
10661112
}
10671113
}
10681114

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

Lines changed: 50 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -825,7 +825,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
825825
unsafe { self.tail.as_mut().map(|node| &mut node.as_mut().element) }
826826
}
827827

828-
/// Adds an element first in the list.
828+
/// Adds an element to the front of the list.
829829
///
830830
/// This operation should compute in *O*(1) time.
831831
///
@@ -844,11 +844,34 @@ impl<T, A: Allocator> LinkedList<T, A> {
844844
/// ```
845845
#[stable(feature = "rust1", since = "1.0.0")]
846846
pub fn push_front(&mut self, elt: T) {
847+
let _ = self.push_front_mut(elt);
848+
}
849+
850+
/// Adds an element to the front of the list, returning a reference to it.
851+
///
852+
/// This operation should compute in *O*(1) time.
853+
///
854+
/// # Examples
855+
///
856+
/// ```
857+
/// #![feature(push_mut)]
858+
/// use std::collections::LinkedList;
859+
///
860+
/// let mut dl = LinkedList::from([1, 2, 3]);
861+
///
862+
/// let ptr = dl.push_front_mut(2);
863+
/// *ptr += 4;
864+
/// assert_eq!(dl.front().unwrap(), &6);
865+
/// ```
866+
#[unstable(feature = "push_mut", issue = "135974")]
867+
#[must_use = "if you don't need a reference to the value, use `LinkedList::push_front` instead"]
868+
pub fn push_front_mut(&mut self, elt: T) -> &mut T {
847869
let node = Box::new_in(Node::new(elt), &self.alloc);
848-
let node_ptr = NonNull::from(Box::leak(node));
870+
let mut node_ptr = NonNull::from(Box::leak(node));
849871
// SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked
850872
unsafe {
851873
self.push_front_node(node_ptr);
874+
&mut node_ptr.as_mut().element
852875
}
853876
}
854877

@@ -876,7 +899,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
876899
self.pop_front_node().map(Node::into_element)
877900
}
878901

879-
/// Appends an element to the back of a list.
902+
/// Adds an element to the back of the list.
880903
///
881904
/// This operation should compute in *O*(1) time.
882905
///
@@ -893,11 +916,34 @@ impl<T, A: Allocator> LinkedList<T, A> {
893916
#[stable(feature = "rust1", since = "1.0.0")]
894917
#[rustc_confusables("push", "append")]
895918
pub fn push_back(&mut self, elt: T) {
919+
let _ = self.push_back_mut(elt);
920+
}
921+
922+
/// Adds an element to the back of the list, returning a reference to it.
923+
///
924+
/// This operation should compute in *O*(1) time.
925+
///
926+
/// # Examples
927+
///
928+
/// ```
929+
/// #![feature(push_mut)]
930+
/// use std::collections::LinkedList;
931+
///
932+
/// let mut dl = LinkedList::from([1, 2, 3]);
933+
///
934+
/// let ptr = dl.push_back_mut(2);
935+
/// *ptr += 4;
936+
/// assert_eq!(dl.back().unwrap(), &6);
937+
/// ```
938+
#[unstable(feature = "push_mut", issue = "135974")]
939+
#[must_use = "if you don't need a reference to the value, use `LinkedList::push_back` instead"]
940+
pub fn push_back_mut(&mut self, elt: T) -> &mut T {
896941
let node = Box::new_in(Node::new(elt), &self.alloc);
897-
let node_ptr = NonNull::from(Box::leak(node));
942+
let mut node_ptr = NonNull::from(Box::leak(node));
898943
// SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked
899944
unsafe {
900945
self.push_back_node(node_ptr);
946+
&mut node_ptr.as_mut().element
901947
}
902948
}
903949

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

Lines changed: 50 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -990,7 +990,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
990990
unsafe { self.tail.as_mut().map(|node| &mut node.as_mut().element) }
991991
}
992992

993-
/// Adds an element first in the list.
993+
/// Adds an element to the front of the list.
994994
///
995995
/// This operation should compute in *O*(1) time.
996996
///
@@ -1009,11 +1009,34 @@ impl<T, A: Allocator> LinkedList<T, A> {
10091009
/// ```
10101010
#[stable(feature = "rust1", since = "1.0.0")]
10111011
pub fn push_front(&mut self, elt: T) {
1012+
let _ = self.push_front_mut(elt);
1013+
}
1014+
1015+
/// Adds an element to the front of the list, returning a reference to it.
1016+
///
1017+
/// This operation should compute in *O*(1) time.
1018+
///
1019+
/// # Examples
1020+
///
1021+
/// ```
1022+
/// #![feature(push_mut)]
1023+
/// use std::collections::LinkedList;
1024+
///
1025+
/// let mut dl = LinkedList::from([1, 2, 3]);
1026+
///
1027+
/// let ptr = dl.push_front_mut(2);
1028+
/// *ptr += 4;
1029+
/// assert_eq!(dl.front().unwrap(), &6);
1030+
/// ```
1031+
#[unstable(feature = "push_mut", issue = "135974")]
1032+
#[must_use = "if you don't need a reference to the value, use `LinkedList::push_front` instead"]
1033+
pub fn push_front_mut(&mut self, elt: T) -> &mut T {
10121034
let node = Box::new_in(Node::new(elt), &self.alloc);
1013-
let node_ptr = NonNull::from(Box::leak(node));
1035+
let mut node_ptr = NonNull::from(Box::leak(node));
10141036
// SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked
10151037
unsafe {
10161038
self.push_front_node(node_ptr);
1039+
&mut node_ptr.as_mut().element
10171040
}
10181041
}
10191042

@@ -1041,7 +1064,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
10411064
self.pop_front_node().map(Node::into_element)
10421065
}
10431066

1044-
/// Appends an element to the back of a list.
1067+
/// Adds an element to the back of the list.
10451068
///
10461069
/// This operation should compute in *O*(1) time.
10471070
///
@@ -1058,11 +1081,34 @@ impl<T, A: Allocator> LinkedList<T, A> {
10581081
#[stable(feature = "rust1", since = "1.0.0")]
10591082
#[rustc_confusables("push", "append")]
10601083
pub fn push_back(&mut self, elt: T) {
1084+
let _ = self.push_back_mut(elt);
1085+
}
1086+
1087+
/// Adds an element to the back of the list, returning a reference to it.
1088+
///
1089+
/// This operation should compute in *O*(1) time.
1090+
///
1091+
/// # Examples
1092+
///
1093+
/// ```
1094+
/// #![feature(push_mut)]
1095+
/// use std::collections::LinkedList;
1096+
///
1097+
/// let mut dl = LinkedList::from([1, 2, 3]);
1098+
///
1099+
/// let ptr = dl.push_back_mut(2);
1100+
/// *ptr += 4;
1101+
/// assert_eq!(dl.back().unwrap(), &6);
1102+
/// ```
1103+
#[unstable(feature = "push_mut", issue = "135974")]
1104+
#[must_use = "if you don't need a reference to the value, use `LinkedList::push_back` instead"]
1105+
pub fn push_back_mut(&mut self, elt: T) -> &mut T {
10611106
let node = Box::new_in(Node::new(elt), &self.alloc);
1062-
let node_ptr = NonNull::from(Box::leak(node));
1107+
let mut node_ptr = NonNull::from(Box::leak(node));
10631108
// SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked
10641109
unsafe {
10651110
self.push_back_node(node_ptr);
1111+
&mut node_ptr.as_mut().element
10661112
}
10671113
}
10681114

0 commit comments

Comments
 (0)