[1718627440]

> That's one of the things named lifetimes let you do, but named lifetimes are flexible enough for more than just that use case, from slightly more complex things like dealing with multiple independent lifetimes at the same time (for example, returning two references instead of just one, or structs/functions using multiple lifetimes), to more obscure stuff like dealing with higher-ranked trait bounds [1].

In SPlint you would describe something as `special` and then describe the individual elements.

> Kind of a tangent, but the manual is a bit unclear to me as to what `returned` is capable of.

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

> Would that be accepted as well?

    $ cat test.c

    int *
    max (/*@returned@*/ int * a, /*@returned@*/ int * b) {
     if (*a > *b) return a; else return b;
    }
    
    int
    main (void)
    {
     int * a = malloc (sizeof *a);
     int * b = malloc (sizeof *b);
     int * c;
    
     if (!a || !b) abort ();
    
     *a = 4;
     *b = 6;
    
     c = max (a, b);
    
     free (a);
     free (b);
     free (c);
     return 0;
    }

    $ splint test.c

    Splint 3.1.1 --- 05 Jan 2023

    Finished checking --- 2 code warnings
    test.c: (in function main)
    test.c:22:8: Dead storage c passed as out parameter to free: c
      Memory is used after it has been released (either by passing as an only param
      or assigning to an only global). (Use -usereleased to inhibit warning)
       test.c:20:8: Storage c released
    test.c:2:1: Function exported but not used outside test: max
      A declaration is exported, but not used outside this module. Declaration can
      use static qualifier. (Use -exportlocal to inhibit warning)
       test.c:4:1: Definition of max

[aw1621107]

> 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]

> 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.

[aw1621107]

> 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],
    }