Skip to content

Commit 80e8822

Browse files
change traitbound for KaniRefIter & KaniPtrIter
1 parent b4bffda commit 80e8822

File tree

2 files changed

+9
-9
lines changed

2 files changed

+9
-9
lines changed

library/kani/src/iter.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
//! while maintaining the semantics of the loop.
77
use crate::{KaniIntoIter, KaniPtrIter};
88

9-
impl<T: Copy> KaniIntoIter for Vec<T> {
9+
impl<T: Clone> KaniIntoIter for Vec<T> {
1010
type Iter = KaniPtrIter<T>;
1111
fn kani_into_iter(self) -> Self::Iter {
1212
let s = self.iter();

library/kani_core/src/iter.rs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -68,24 +68,24 @@ macro_rules! generate_iter {
6868
fn len(&self) -> usize;
6969
}
7070

71-
pub struct KaniPtrIter<T: Copy> {
71+
pub struct KaniPtrIter<T> {
7272
pub ptr: *const T,
7373
pub len: usize,
7474
}
7575

76-
impl<T: Copy> KaniPtrIter<T> {
76+
impl<T: Clone> KaniPtrIter<T> {
7777
pub fn new(ptr: *const T, len: usize) -> Self {
7878
KaniPtrIter { ptr, len }
7979
}
8080
}
8181

82-
impl<T: Copy> KaniIter for KaniPtrIter<T> {
82+
impl<T: Clone> KaniIter for KaniPtrIter<T> {
8383
type Item = T;
8484
fn nth(&self, i: usize) -> Self::Item {
85-
unsafe { *self.ptr.wrapping_add(i) }
85+
unsafe { (&*self.ptr.wrapping_add(i)).clone() }
8686
}
8787
fn first(&self) -> Self::Item {
88-
unsafe { *self.ptr }
88+
unsafe { (&*self.ptr).clone() }
8989
}
9090
fn assumption(&self) -> bool {
9191
//SAFETY: this call is safe as Rust compiler will complain if we write a for-loop for initnitialized object
@@ -96,19 +96,19 @@ macro_rules! generate_iter {
9696
}
9797
}
9898

99-
pub struct KaniRefIter<'a, T: Copy> {
99+
pub struct KaniRefIter<'a, T> {
100100
pub ptr: *const T,
101101
pub len: usize,
102102
_marker: PhantomData<&'a T>,
103103
}
104104

105-
impl<'a, T: Copy> KaniRefIter<'a, T> {
105+
impl<'a, T> KaniRefIter<'a, T> {
106106
pub fn new(ptr: *const T, len: usize) -> Self {
107107
KaniRefIter { ptr, len, _marker: PhantomData }
108108
}
109109
}
110110

111-
impl<'a, T: Copy> KaniIter for KaniRefIter<'a, T> {
111+
impl<'a, T> KaniIter for KaniRefIter<'a, T> {
112112
type Item = &'a T;
113113
fn nth(&self, i: usize) -> Self::Item {
114114
unsafe { &*self.ptr.wrapping_add(i) }

0 commit comments

Comments
 (0)