generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 134
Closed
Labels
T-UserTag user issues / requestsTag user issues / requests[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.
Description
Proposed change:
Implement kani::Arbitrary for PhantomData<T> (blanket impl for all T) and PhantomPinned
Motivation:
I have a struct which represents "bytes that can be deserialized to a T":
struct TypedBytes<'a, T> {
bytes: &'a [u8],
_marker: core::marker::PhantomData<T>,
}I'd like to be able to use #[cfg_attr(kani, derive(kani::Arbitrary))] on this struct, but currently I can't since PhantomData doesn't implement Arbitrary.
Since they are ZSTs, there are no values of either type, so presumably don't interact with symbolic values? I can't see a harm in allowing this, but I'm not familiar with kani, so let me know if I'm not understanding something 😁
Thanks
Metadata
Metadata
Assignees
Labels
T-UserTag user issues / requestsTag user issues / requests[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.