[splint-discuss] SPlint should recognize POSIX select(2)

[Roland Illig]

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 
Foo_init().

void Foo_finalize(Foo *foo)
	/*@requires defined foo; @*/
	/*@ensures undefined foo; @*/;

Roland