[splint-discuss] Extensible checking for scanf

[Ibéria Medeiros]

HI,

I have been work around with extensible checking (chapter 10 in splint
manual) to tainted input variables. My goal is taint any input
variable. For that, i create the attribute inputness, with context
reference, with 2 states - tainted and untainted, with 2 annotations
inputtainted and inputuntainted, respectevely.

i specify what input functions i want ensure that returned variable is
inputtainted. For example,

extern char *fgets (/*@returned@*/ char *s, int n, FILE *stream)
  /*@ensures inputtainted s@*/;
(here i grant that s will be tainted)

extern /*@inputtainted@*/ int getchar(void)
/*@ensures inputtainted@*/;
(here i grant that returned value is tainted)

but, for scanf function how i can grant that returned variable is inputtainted??

In a first approach i define scanf:
extern int scanf(const char *format, ...)
  /*@ensures inputtainted ...@*/;

but splint give me a parse error, because dont accept "..." parameter

any help?

regards,

-- 
Ibéria Medeiros