[splint-discuss] tainted analysis with splint

[Ibéria Medeiros]

Hi,

i am trying make tainted analysis with splint, across extensible checking.
My support for do that is the example tainted.mts (come with splint tool),
where the principal purpose is detect format string bugs.

My goal for tainted analysis is signalize every input variables, read across
input functions, with tainted state.  I create the attribute taintness (file
.mts) and create the file .xh with every input functions, where i annotated
every returned parameters with tainted annotation. For example,

extern char *fgets (/*@returned@*/ char *s, int n, FILE *stream)
  /*@ensures tainted s@*/;

in fgets function i ensure *s is tainted.

My problem is how can i do that to function scanf or sscanf, where the
returned parameter is ... (extern int scanf(const char *format, ...))

I have trying the next declaration, but splint give me a error

extern int scanf(const char *format, ...)
  /*@ensures tainted ...@*/;

any help, please

regards

-- 
Ibéria Medeiros
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.cs.virginia.edu/pipermail/splint-discuss/attachments/20071004/bffbf9c5/attachment-0001.html