points
6 days ago
| 1 comment
| HN
> In SPlint you would describe something as `special` and then describe the individual elements.

Interesting. That does seem to provide more flexibility, though based on what the manual says I still feel like it's not quite to the same level as named lifetimes since `special` looks like it revolves around allocation/initialization?

At least based on a quick skim of the manual structs with non-owning pointers still seems like a potential difference since from what I can tell struct field checks are either for ownership (/@only@/ for fields by default), initialization/allocation (`partial`, state clauses), or requires overhead (/@refs@/). Nothing quite like "the data here will live for some arbitrary lifetime(s) dictated by the use context".

> Aliasing is mutual and storage refers to the region an object lives. It doesn't refer to exact pointer values.

I... think that answers my question? Some quick tests seem to bear that out as well.

> $ cat test.c

So I think I'm a bit dim and for some reason I thought Splint was not free. Sorry for the bother! I could have tried things out myself this entire time!

Good to see that /@returned@/ works like I hoped at least.

▲
1718627440
5 days ago
[-]
> At least based on a quick skim of the manual structs with non-owning pointers still seems like a potential difference since from what I can tell struct field checks are either for ownership (/@only@/ for fields by default), initialization/allocation (`partial`, state clauses), or requires overhead (/@refs@/). Nothing quite like "the data here will live for some arbitrary lifetime(s) dictated by the use context".

Then I don't understand (your/Rusts) understanding of lifetimes. 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 thought Splint was not free

It is for example in Debian, but I have recompiled it myself, since the Debian version has some bugs.

reply
▲
aw1621107
5 days ago
[-]
> 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):

    struct ByteSlices<'a, 'b> {
        first: &'a [u8],
        second: &'b [u8],
    }
reply