[splint-discuss] SPlint should recognize POSIX select(2)
roland.illig at gmx.de
Thu Sep 23 03:50:42 EDT 2004
David Evans wrote:
> On Thu, 23 Sep 2004, Roland Illig wrote:
>>Another question: Is it possible to declare a function that /*@ensures
>>undefined foo; @*/ to mark foo object as undefined, but allocated?
>>void Foo_finalize(Foo *foo)
>> /*@ensures undefined foo; @*/;
> Yes, the /*@out@*/ annotation means this. You can also use
> /*@allocates foo;@*/
> See http://www.splint.org/manual/html/sec7.html (Section 7.4) for details.
No, that's not what I want. As the name Foo_finalize suggests, foo shall
be completely defined before and is undefined, but _still_ allocated
after the function call.
I thought the /*@out@*/ annotation was the other way round, suited for
void Foo_finalize(Foo *foo)
/*@requires defined foo; @*/
/*@ensures undefined foo; @*/;
More information about the splint-discuss