> As to my understanding, the lifetime of an object is bound by the lifetime of the underlying allocation and is the time during which the storage of the allocation is initialized without interruption.
I think that's more or less the same definition used by Rust. It's just that the borrow checker gives you some more options to use/manipulate lifetimes.
Not entirely sure this would help, the consider this type from earlier:
struct ByteSlice<'a> {
slice: &'a [u8],
}
This describes a struct containing a non-owning reference to a slice of bytes where the reference has some "placeholder" lifetime 'a (where 'a could be checked at the point of use and in a more abstract way without necessarily knowing about an actual underlying object). This could be handy if you need to refer to multiple subsets of a whole and don't want to make a copy - say, if you were writing a zero-copy parser. The borrow checker will ensure that the underlying data will always be valid for as long as this struct is used.
I didn't see an obvious analogous annotation in the Splint user manual that lets it check this kind of construct. This struct doesn't own the data it references, so /*@only@*/ doesn't apply. The reference itself as well as the data it references will be initialized since `MaybeUninit` isn't involved, so `partial` and state clauses don't apply. And no reference counting is involved, so /*@refs@*/ doesn't apply either. `dependent` seems like it might fit, but that isn't checked.
The names also let you be more specific with your lifetimes. For example, you could create a struct with references with two different but overlapping lifetimes (though I think such cases would be rare in practice):
I think that's more or less the same definition used by Rust. It's just that the borrow checker gives you some more options to use/manipulate lifetimes.
Not entirely sure this would help, the consider this type from earlier:
This describes a struct containing a non-owning reference to a slice of bytes where the reference has some "placeholder" lifetime 'a (where 'a could be checked at the point of use and in a more abstract way without necessarily knowing about an actual underlying object). This could be handy if you need to refer to multiple subsets of a whole and don't want to make a copy - say, if you were writing a zero-copy parser. The borrow checker will ensure that the underlying data will always be valid for as long as this struct is used.I didn't see an obvious analogous annotation in the Splint user manual that lets it check this kind of construct. This struct doesn't own the data it references, so /*@only@*/ doesn't apply. The reference itself as well as the data it references will be initialized since `MaybeUninit` isn't involved, so `partial` and state clauses don't apply. And no reference counting is involved, so /*@refs@*/ doesn't apply either. `dependent` seems like it might fit, but that isn't checked.
The names also let you be more specific with your lifetimes. For example, you could create a struct with references with two different but overlapping lifetimes (though I think such cases would be rare in practice):