#ifndef STRICT, an /*@alt void@*/ annotion is applied to the return types of fprintf, printf, and sprintf in lib/standard.h. Why are other *printf functions (such as vprintf) not so annotated?
#if 1, memcpy, memmove and memset are similarly annotated. I was about to ask about strcpy but see it is declared as void /*@alt char * @*/... I infer that the reason for not using #ifdef STRICT on these is that ignoring the return codes does not scrap any information. Why are two techniques used for marking void alternatives? I would like to alter this standard, default behaviour. How, for example, would I allow the return code of fclose to be ignored for a particular run of splint? (void)fclose is a bit permanent; -retvalint would - presumably - also affect fscanf. A commercial product produces message 534 in such cases and allows -esym(534,fclose) to do what I want. If my code contains a declaration of fclose which allows a null return, I get "Parse Error: Inconsistent function declaration". "int foo(); int foo(int bar);" is OK. Why not allow "int foo(); int foo /*@alt void@*/();"? -- Walter Briscoe