*** empty log message ***

diff --git a/test/tainted/Makefile b/test/tainted/Makefile
index 1d0c0dd2d1e38cd6b6af23e272929e515d623f6f..2c57fd8bb446c8f646c94942fd9fc12b3a33cbff 100644 (file)
--- a/test/tainted/Makefile
+++ b/test/tainted/Makefile
@@ -13,3 +13,4 @@ tainted:
        ${LCLINT} -mts tainted tainted5.c -mustfree -exportlocal
        ${LCLINT} -mts tainted taintedmerge.c -mustfree -exportlocal -expect 3
        ${LCLINT} -mts tainted taintedimplicit.c -mustfree -exportlocal -expect 1
+       ${LCLINT} -mts tainted sprintf.c -expect 2

diff --git a/test/tainted/sprintf.c b/test/tainted/sprintf.c
new file mode 100644 (file)
index 0000000..d8abded
--- /dev/null
+++ b/test/tainted/sprintf.c
@@ -0,0 +1,18 @@
+char *sp (/*@untainted@*/ char *s1, /*@untainted@*/ char *s2, /*@tainted@*/ char *s3)
+{
+  char *s;
+  s = (char *) malloc (sizeof (*s) * 100);
+  assert (s != NULL);
+
+  sprintf (s, "%s %d %s %d", s1, 3, s2, 3);
+  (void) system (s); /* okay */
+
+  sprintf (s, "%s %d %s %d", s1, 3, s3, 3);
+  (void) system (s); /* error */
+
+  sprintf (s, "%s %d %s %d %s %s %s", s1, 3, s2, 3, s2, s3, s2);
+  (void) system (s); /* error */
+
+  return s; /* error */
+}
+  

diff --git a/test/tainted/tainted.xh b/test/tainted/tainted.xh
index 6d7f521f32e7a52d3fb7d5cccd85f06890f90158..a6f9c52e66f840aec54138edb86529469d56a438 100644 (file)
--- a/test/tainted/tainted.xh
+++ b/test/tainted/tainted.xh
@@ -11,6 +11,9 @@ extern /*@observer@*/ char *tmpnam (/*@untainted@*/ char *s) ;
 
 extern FILE *fopen (/*@untainted@*/ char *filename, char *mode) ;
 
+extern int sprintf (/*@out@*/ char *s, /*@untainted@*/ char *format, ...) 
+   /*@ensures s:taintedness = ...:taintedness@*/ ;
+
 extern int printf (/*@untainted@*/ char *format, ...) ;
 
 extern /*@null@*/ FILE *freopen (/*@untainted@*/ char *filename, char *mode, FILE *stream) ;