[splint-discuss] The "errorcode" annotation

[Austin Hastings]

--- "Jay A. St. Pierre" <Jay.St.Pierre at colorado.edu> wrote:
> I noticed that some of the standard functions are annotated with 
> an "errorcode" annotation.  For example, in standard.h, there is 
> the following:
> 
> void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char
> *buf)
>      /*@modifies fileSystem, *stream, *buf@*/
>      /*:errorcode != 0*/ ;
>      /*:requires maxSet(buf) >= (BUFSIZ - 1):*/ ;
> 
> What does the "errorcode" annotation do?  I haven't found any 
> documentation of it.

Based on simple visual inspection, the overall purpose of errorcode
seems to be a description of the behavior of the function when an error
occurs. (Possibly intended to provide detection of mishandled return
values?)

Regardless, the setbuf function returns void, so in this case the
errorcode description is wrong. You've discovered an undocumented
feature and an apparent bug at the same time.

=Austin