From: evans <evans>
Date: Tue, 24 Jul 2001 18:55:39 +0000 (+0000)
Subject: *** empty log message ***
X-Git-Tag: Alpha-3_0_0_19~82
X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/commitdiff_plain/98ed3b22cc6220600844f91bf4167eebd0457a3f

*** empty log message ***
---

diff --git a/test/mergestate.expect b/test/mergestate.expect
new file mode 100644
index 0000000..6fbe92e
--- /dev/null
+++ b/test/mergestate.expect
@@ -0,0 +1,22 @@
+
+taintednm.c: (in function f)
+taintednm.c:15:7: Attributes merged in ensures clause in states that cannot be
+                     combined (t2 is untainted, s is tainted): bogus merge
+   taintednm.c:1:32: Meta state s becomes tainted
+taintednm.c:24:10: Stack-allocated storage t reachable from return value: t
+
+Finished LCLint checking --- 2 code errors found, as expected
+
+taintednm.c: (in function f)
+taintednm.c:16:18: Invalid transfer from tainted t to untainted (Possibly
+                      tainted storage used as untainted.): t
+   taintednm.c:15:7: Meta state t becomes tainted
+taintednm.c:19:18: Invalid transfer from tainted t to untainted (Possibly
+                      tainted storage used as untainted.): t
+   taintednm.c:18:7: Meta state t becomes tainted
+taintednm.c:22:18: Invalid transfer from tainted t to untainted (Possibly
+                      tainted storage used as untainted.): t
+   taintednm.c:18:7: Meta state t becomes tainted
+taintednm.c:24:10: Stack-allocated storage t reachable from return value: t
+
+Finished LCLint checking --- 4 code errors found, as expected
diff --git a/test/mystrncat.c b/test/mystrncat.c
new file mode 100644
index 0000000..055cd2c
--- /dev/null
+++ b/test/mystrncat.c
@@ -0,0 +1,18 @@
+void  mystrncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, int n)
+     /*@modifies *s1@*/ /*@requires MaxSet(s1) >= ( MaxRead(s1) + n); @*/
+     /*@ensures MaxRead(result) >= (MaxRead(s1) + n); @*/;
+
+     void func(char *str)
+{
+  char buffer[256];
+  char *b;
+
+  b = malloc(256);
+  assert(b != NULL);
+  mystrncat(buffer, str, sizeof(buffer) - 1);
+  mystrncat(b, str, sizeof(buffer) - 1);
+
+  free (b);
+  return;
+}
+
diff --git a/test/mystrncat.expect b/test/mystrncat.expect
new file mode 100644
index 0000000..11fbb87
--- /dev/null
+++ b/test/mystrncat.expect
@@ -0,0 +1,22 @@
+
+mystrncat.c: (in function func)
+mystrncat.c:12:13: Passed storage buffer not completely defined (*buffer is
+                      undefined): mystrncat (buffer, ...)
+mystrncat.c:13:13: Passed storage b not completely defined (*b is undefined):
+                      mystrncat (b, ...)
+mystrncat.c:13:3: Unresolved constraint:
+    Lclint is unable to resolve Requires: :
+    MAXREAD ((malloc(256) @ mystrncat.c:10:7 ) )  <=  ( 0 )  needed to satisfy
+    Requires: : MAXSET ((b @ mystrncat.c:13:13 ) )  >=  (MAXREAD ((b @
+    mystrncat.c:13:13 ) )) + (( 255 ) ) derived from mystrncat precondition:
+    Requires: : MAXSET ((<parameter 1> ) )  >=  (MAXREAD ((<parameter 1> ) )) +
+    ((<parameter 3> ) )
+mystrncat.c:12:3: Unresolved constraint:
+    Lclint is unable to resolve Requires: : MAXREAD ((buffer @
+    mystrncat.c:12:13 ) )  <=  ( 0 )  needed to satisfy Requires: :
+    MAXSET ((buffer @ mystrncat.c:12:13 ) )  >=  (MAXREAD ((buffer @
+    mystrncat.c:12:13 ) )) + (( 255 ) ) derived from mystrncat precondition:
+    Requires: : MAXSET ((<parameter 1> ) )  >=  (MAXREAD ((<parameter 1> ) )) +
+    ((<parameter 3> ) )
+
+Finished LCLint checking --- 4 code errors found, as expected
diff --git a/test/mystrncat.out b/test/mystrncat.out
new file mode 100644
index 0000000..490d7e3
--- /dev/null
+++ b/test/mystrncat.out
@@ -0,0 +1,24 @@
+
+mystrncat.c: (in function func)
+mystrncat.c:12:13: Passed storage buffer not completely defined (*buffer is
+                      undefined): mystrncat (buffer, ...)
+mystrncat.c:13:13: Passed storage b not completely defined (*b is undefined):
+                      mystrncat (b, ...)
+mystrncat.c:13:3: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : maxRead ((malloc(256) @ mystrncat.c:10:7 ) )  <=  ( 0 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((b @ mystrncat.c:13:13 ) )  >=  (maxRead ((b @
+    mystrncat.c:13:13 ) )) + (( 255 ) )
+     derived from mystrncat precondition: requires: :
+    maxSet ((<parameter 1> ) )  >=  (maxRead ((<parameter 1> ) )) +
+    ((<parameter 3> ) )
+mystrncat.c:12:3: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : maxRead ((buffer @ mystrncat.c:12:13 ) )  <=  ( 0 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((buffer @ mystrncat.c:12:13 ) )  >=  (maxRead ((buffer
+    @ mystrncat.c:12:13 ) )) + (( 255 ) )
+     derived from mystrncat precondition: requires: :
+    maxSet ((<parameter 1> ) )  >=  (maxRead ((<parameter 1> ) )) +
+    ((<parameter 3> ) )
+
+Finished LCLint checking --- 4 code errors found, as expected
diff --git a/test/noeffect.c b/test/noeffect.c
new file mode 100644
index 0000000..a820c70
--- /dev/null
+++ b/test/noeffect.c
@@ -0,0 +1,4 @@
+typedef char *exprNode;
+/*@function void exprNode_swap (sef exprNode, sef exprNode)@*/
+# define exprNode_swap(e1,e2) do { exprNode m_tmp = (e1); (e1) = (e2); (e2) = m_tmp; } while (FALSE)
+
diff --git a/test/noeffect.expect b/test/noeffect.expect
new file mode 100644
index 0000000..e0fb16a
--- /dev/null
+++ b/test/noeffect.expect
@@ -0,0 +1,14 @@
+/af10/evans/LCLintDev/src/lclint noeffect.c +allmacros +checks -expect 3
+
+noeffect.c: (in macro exprNode_swap)
+noeffect.c:3:59: Assignment to macro parameter: e1
+  A macro parameter is used as the left side of an assignment expression. This
+  exhibits behavior that could not be implemented by a function. (-macroassign
+  will suppress message)
+noeffect.c:3:72: Assignment to macro parameter: e2
+noeffect.c:2:18: File static function exprNode_swap declared but not used
+  A function is declared but not used. Use /*@unused@*/ in front of function
+  header to suppress message. (-fcnuse will suppress message)
+   noeffect.c:3: Definition of exprNode_swap
+
+Finished LCLint checking --- 3 code errors found, as expected
diff --git a/test/noeffect.out b/test/noeffect.out
new file mode 100644
index 0000000..e0fb16a
--- /dev/null
+++ b/test/noeffect.out
@@ -0,0 +1,14 @@
+/af10/evans/LCLintDev/src/lclint noeffect.c +allmacros +checks -expect 3
+
+noeffect.c: (in macro exprNode_swap)
+noeffect.c:3:59: Assignment to macro parameter: e1
+  A macro parameter is used as the left side of an assignment expression. This
+  exhibits behavior that could not be implemented by a function. (-macroassign
+  will suppress message)
+noeffect.c:3:72: Assignment to macro parameter: e2
+noeffect.c:2:18: File static function exprNode_swap declared but not used
+  A function is declared but not used. Use /*@unused@*/ in front of function
+  header to suppress message. (-fcnuse will suppress message)
+   noeffect.c:3: Definition of exprNode_swap
+
+Finished LCLint checking --- 3 code errors found, as expected
diff --git a/test/tainted/Bad: b/test/tainted/Bad:
new file mode 100644
index 0000000..e69de29
diff --git a/test/tainted/Makefile b/test/tainted/Makefile
new file mode 100644
index 0000000..1d0c0dd
--- /dev/null
+++ b/test/tainted/Makefile
@@ -0,0 +1,15 @@
+.PHONY: tainted 
+
+LCLINT = lclint
+
+all: tainted 
+
+tainted:
+	${LCLINT} -mts tainted tainted.c -mustfree -exportlocal -expect 4
+	${LCLINT} tainted-bad.mts tainted.xh tainted.c -mustfree -exportlocal -expect 9
+	${LCLINT} -mts tainted tainted2.c -mustfree -exportlocal -expect 1
+	${LCLINT} -mts tainted tainted3.c -mustfree -exportlocal -expect 1
+	${LCLINT} -mts tainted tainted4.c -mustfree -exportlocal -expect 1
+	${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
diff --git a/test/tainted/Makefile~ b/test/tainted/Makefile~
new file mode 100644
index 0000000..82571ac
--- /dev/null
+++ b/test/tainted/Makefile~
@@ -0,0 +1,15 @@
+.PHONY: tainted 
+
+LCLINT = lclint
+
+all: tainted 
+
+tainted:
+	${LCLINT} -mts tainted tainted.c -mustfree -exportlocal -expect 4
+	${LCLINT} tainted-bad.mts tainted.xh tainted.c -mustfree -exportlocal -expect 9
+	${LCLINT} -mts tainted tainted2.c -mustfree -exportlocal -expect 1
+	${LCLINT} -mts tainted tainted3.c -mustfree -exportlocal -expect 1
+	${LCLINT} -mts tainted tainted4.c -mustfree -exportlocal -expect 1
+	${LCLINT} -mts tainted tainted5.c -mustfree -exportlocal -expect 2
+	${LCLINT} -mts tainted taintedmerge.c -mustfree -exportlocal -expect 3
+	${LCLINT} -mts tainted taintedimplicit.c -mustfree -exportlocal -expect 1
diff --git a/test/tainted/t1.c b/test/tainted/t1.c
new file mode 100644
index 0000000..e70d16d
--- /dev/null
+++ b/test/tainted/t1.c
@@ -0,0 +1,6 @@
+extern char *mtainted (char *s); 
+
+void test (/*@untainted@*/ char *s)
+{
+  (void) system (mtainted (s));
+}
diff --git a/test/tainted/t1.c~ b/test/tainted/t1.c~
new file mode 100644
index 0000000..20e1067
--- /dev/null
+++ b/test/tainted/t1.c~
@@ -0,0 +1,21 @@
+extern char *mtainted (char *s); 
+
+/*@untainted@*/ char *f (/*@tainted@*/ char *s, /*@untainted@*/ char *us)
+{
+  char *x = f (us, s); /* Error: tainted as untainted */
+  return f (x, us);
+}
+
+void test (/*@tainted@*/ char *s)
+{
+  char *t = malloc (sizeof (char) * strlen (s));
+  (void) system (s); /* error */
+
+  assert (t != NULL);
+  strcpy (t, s);
+  /* t is tainted too */
+  (void) system (t); /* error */
+
+  t = mtainted (s); /* default return is tainted! */
+  (void) system (t); /* error */
+}
diff --git a/test/tainted/tainted-bad.mts b/test/tainted/tainted-bad.mts
new file mode 100644
index 0000000..d7953a2
--- /dev/null
+++ b/test/tainted/tainted-bad.mts
@@ -0,0 +1,23 @@
+attribute taintedness
+   context reference
+   oneof untainted, tainted, untainted
+   defaults 
+      reference ==> stainted
+      parameter ==> tainted
+      parameter ==> untainted
+   annotations
+      tainted reference ==> tainted
+      untainted reference ==> untainted
+      maybetainted reference ==> blue
+   merge
+      tainted + * ==> tainted
+      tainted + junky ==> error "Splat!"
+   transfers
+      tainted as untainted ==> error "Possibly tainted storage used as untainted."
+      tainted as tainted ==> tainted
+      untainted as tainted ==> peach
+      untainted as untainted ==> untainted
+end
+
+
+
diff --git a/test/tainted/tainted.c b/test/tainted/tainted.c
new file mode 100644
index 0000000..20e1067
--- /dev/null
+++ b/test/tainted/tainted.c
@@ -0,0 +1,21 @@
+extern char *mtainted (char *s); 
+
+/*@untainted@*/ char *f (/*@tainted@*/ char *s, /*@untainted@*/ char *us)
+{
+  char *x = f (us, s); /* Error: tainted as untainted */
+  return f (x, us);
+}
+
+void test (/*@tainted@*/ char *s)
+{
+  char *t = malloc (sizeof (char) * strlen (s));
+  (void) system (s); /* error */
+
+  assert (t != NULL);
+  strcpy (t, s);
+  /* t is tainted too */
+  (void) system (t); /* error */
+
+  t = mtainted (s); /* default return is tainted! */
+  (void) system (t); /* error */
+}
diff --git a/test/tainted/tainted.mts b/test/tainted/tainted.mts
new file mode 100644
index 0000000..4f8198e
--- /dev/null
+++ b/test/tainted/tainted.mts
@@ -0,0 +1,22 @@
+attribute taintedness
+   context reference char *
+   oneof untainted, tainted
+   annotations
+      tainted reference ==> tainted
+      untainted reference ==> untainted
+   transfers
+      tainted as untainted ==> error "Possibly tainted storage used as untainted."
+      untainted as tainted ==> untainted
+   merge
+      tainted + untainted ==> tainted
+      /*untainted + tainted ==> tainted */
+   defaults 
+      reference ==> untainted
+      parameter ==> tainted
+      result ==> tainted /* Different from lib/tainted.mts */
+      literal ==> untainted
+      null ==> untainted 
+end
+
+
+
diff --git a/test/tainted/tainted.mts~ b/test/tainted/tainted.mts~
new file mode 100644
index 0000000..5b0163f
--- /dev/null
+++ b/test/tainted/tainted.mts~
@@ -0,0 +1,22 @@
+attribute taintedness
+   context reference char *
+   oneof untainted, tainted
+   annotations
+      tainted reference ==> tainted
+      untainted reference ==> untainted
+   transfers
+      tainted as untainted ==> error "Possibly tainted storage used as untainted."
+      untainted as tainted ==> untainted
+   merge
+      tainted + untainted ==> tainted
+      /*untainted + tainted ==> tainted */
+   defaults 
+      reference ==> tainted
+      parameter ==> tainted
+      result ==> tainted
+      literal ==> untainted
+      null ==> untainted 
+end
+
+
+
diff --git a/test/tainted/tainted.xh b/test/tainted/tainted.xh
new file mode 100644
index 0000000..6d7f521
--- /dev/null
+++ b/test/tainted/tainted.xh
@@ -0,0 +1,31 @@
+/*
+** tainted.xh
+*/
+
+/* Library functions annotated for tainted.mts */
+
+extern int remove (/*@untainted@*/ char *filename) /*@modifies fileSystem, errno@*/ ;
+extern int rename (/*@untainted@*/ char *old, /*@untainted@*/ char *new) ;
+
+extern /*@observer@*/ char *tmpnam (/*@untainted@*/ char *s) ;
+
+extern FILE *fopen (/*@untainted@*/ char *filename, char *mode) ;
+
+extern int printf (/*@untainted@*/ char *format, ...) ;
+
+extern /*@null@*/ FILE *freopen (/*@untainted@*/ char *filename, char *mode, FILE *stream) ;
+
+extern /*@null@*/ /*@tainted@*/ char *
+  fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream) 
+  /*@ensures tainted s@*/ 
+  /*@modifies *s@*/ ;
+
+extern int system (/*@untainted@*/ /*@null@*/ char *s) /*@modifies fileSystem@*/ ;
+
+extern char *strcpy (/*@returned@*/ char *s1, char *s2) 
+  /*@ensures s1:taintedness = s2:taintedness@*/ ;
+
+extern char *strcat (/*@returned@*/ char *s1, char *s2) 
+  /*@ensures s1:taintedness = s1:taintedness | s2:taintedness@*/ 
+  /*:ensures result:tainted = s1:tainted, s2:tainted)@*/ ;
+
diff --git a/test/tainted/tainted2.c b/test/tainted/tainted2.c
new file mode 100644
index 0000000..c822cff
--- /dev/null
+++ b/test/tainted/tainted2.c
@@ -0,0 +1,21 @@
+# include <assert.h>
+
+/*@untainted@*/ char *test (int fromuser, /*@untainted@*/ char *def)
+{
+  char *stk = NULL;
+
+  if (fromuser != 0)
+    {
+      stk = malloc (sizeof (char) * strlen (def));
+      assert (stk != NULL);
+      strcpy (stk, def);
+    }
+  else
+    {
+      stk = malloc (sizeof (char) * 128);
+      assert (stk != NULL);
+      (void) fgets (stk, 128, stdin);
+    }
+
+  return stk;
+}
diff --git a/test/tainted/tainted3.c b/test/tainted/tainted3.c
new file mode 100644
index 0000000..69024f5
--- /dev/null
+++ b/test/tainted/tainted3.c
@@ -0,0 +1,8 @@
+extern void checkUntainted (/*@untainted@*/ char *s) ;
+extern void checkTainted (/*@tainted@*/ char *s) ;
+
+void test (/*@tainted@*/ char *def)
+{
+  checkTainted (def);
+  checkUntainted (def); /* error */
+}
diff --git a/test/tainted/tainted3.c~ b/test/tainted/tainted3.c~
new file mode 100644
index 0000000..196c6eb
--- /dev/null
+++ b/test/tainted/tainted3.c~
@@ -0,0 +1,8 @@
+extern void checkUntainted (char *s) /*@requires untainted s@*/;
+extern void checkTainted (char *s) /*@requires tainted s@*/;
+
+void test (/*@tainted@*/ char *def)
+{
+  checkTainted (def);
+  checkUntainted (def); /* error */
+}
diff --git a/test/tainted/tainted4.c b/test/tainted/tainted4.c
new file mode 100644
index 0000000..ff4cc33
--- /dev/null
+++ b/test/tainted/tainted4.c
@@ -0,0 +1,10 @@
+typedef /*@untainted@*/ char *ucharp_t;
+extern void checkUntainted (ucharp_t *s) ;
+typedef /*@tainted@*/ char *tcharp_t;
+extern void checkTainted (tcharp_t *s) ;
+
+void test (/*@tainted@*/ char *def)
+{
+  checkTainted (&def); /* okay */
+  checkUntainted (&def); /* error */
+}
diff --git a/test/tainted/tainted4.c~ b/test/tainted/tainted4.c~
new file mode 100644
index 0000000..9dfbf89
--- /dev/null
+++ b/test/tainted/tainted4.c~
@@ -0,0 +1,10 @@
+extern void checkUntainted (char **s) /*@requires untainted *s@*/;
+
+typedef /*@tainted@*/ char *charpt;
+extern void checkTainted (charpt *s) ; /* requires tainted *s doesn't work because of implicit annotation! */
+
+void test (/*@tainted@*/ char *def)
+{
+  checkTainted (&def);
+  checkUntainted (&def); /* error */
+}
diff --git a/test/tainted/tainted5.c b/test/tainted/tainted5.c
new file mode 100644
index 0000000..4309eaf
--- /dev/null
+++ b/test/tainted/tainted5.c
@@ -0,0 +1,16 @@
+typedef /*@untainted@*/ char *ucharp_t;
+extern void checkUntainted (ucharp_t *s) ;
+typedef /*@tainted@*/ char *tcharp_t;
+extern void checkTainted (tcharp_t *s) ;
+
+void test (/*@untainted@*/ char *def) 
+{
+  checkUntainted (&def); 
+  checkTainted (&def); /* okay (untainted as tainted) */
+}
+
+void test2 (ucharp_t *def)  
+{
+  checkUntainted (def); 
+  checkTainted (def); /* okay */
+}
diff --git a/test/tainted/tainted5.c~ b/test/tainted/tainted5.c~
new file mode 100644
index 0000000..5339e17
--- /dev/null
+++ b/test/tainted/tainted5.c~
@@ -0,0 +1,14 @@
+extern void checkUntainted (char **s) /*@requires untainted *s@*/;
+extern void checkTainted (char **s) /*@requires tainted *s@*/;
+
+void test (char *def) /*@requires untainted def@*/ 
+{
+  checkUntainted (&def); 
+  checkTainted (&def); /* error */
+}
+
+void test2 (char **def) /*@requires untainted *def@*/ 
+{
+  checkUntainted (def); 
+  checkTainted (def); /* error */
+}
diff --git a/test/tainted/taintedimplicit.c b/test/tainted/taintedimplicit.c
new file mode 100644
index 0000000..b8f0452
--- /dev/null
+++ b/test/tainted/taintedimplicit.c
@@ -0,0 +1,18 @@
+char *taintme (char *s)
+     /*@ensures result:taintedness = s:taintedness@*/
+{
+  char *res = (char *) malloc (sizeof (*res) * strlen (s));
+  assert (res != NULL);
+  strcpy (res, s);
+  return res;
+}
+
+void safecall (/*@untainted@*/ char *s)
+{
+  (void) system (taintme (s)); /* okay */
+}
+
+void dangerouscall (/*@tainted@*/ char *s)
+{
+  (void) system (taintme (s)); /* error */
+}
diff --git a/test/tainted/taintedimplicit.c~ b/test/tainted/taintedimplicit.c~
new file mode 100644
index 0000000..0726e0a
--- /dev/null
+++ b/test/tainted/taintedimplicit.c~
@@ -0,0 +1,8 @@
+char *taintme (char *s)
+     /*@ensures result:taintedness = s:taintedness@*/
+{
+  char *res = (char *) malloc (sizeof (*res) * strlen (s));
+
+  strcpy (res, s);
+  return s;
+}
diff --git a/test/tainted/taintedmerge.c b/test/tainted/taintedmerge.c
new file mode 100644
index 0000000..858990f
--- /dev/null
+++ b/test/tainted/taintedmerge.c
@@ -0,0 +1,17 @@
+char *f (/*@tainted@*/ char *s)
+{
+  char t[50];
+
+  (void) system ("test"); 
+  strcpy (t, "test");
+
+  (void) system (t);
+
+  strcat (t, s);
+  (void) system (t); /* error */
+
+  strcpy (t, s);
+  (void) system (t); /* error */
+
+  return t; /* error - tainted, stack-allocated */
+}
diff --git a/test/tainted/taintedmerge.c~ b/test/tainted/taintedmerge.c~
new file mode 100644
index 0000000..d6cef7b
--- /dev/null
+++ b/test/tainted/taintedmerge.c~
@@ -0,0 +1,12 @@
+char *f (/*@tainted@*/ char *s)
+{
+  char t[50];
+
+  strcpy (t, "test");
+
+  (void) system (t);
+
+  strcat (t, s);
+  
+  (void) system (t); /* error */
+}
diff --git a/test/tainted/taintedx.c b/test/tainted/taintedx.c
new file mode 100644
index 0000000..e37bfb0
--- /dev/null
+++ b/test/tainted/taintedx.c
@@ -0,0 +1,17 @@
+extern void checkUntainted (char **s) /*@requires untainted *s@*/;
+extern void checkUntainted1 (char **s) /*@requires untainted *s@*/;
+extern void checkTainted (char **s) /*@requires tainted *s@*/;
+extern void checkTainted1 (char **s) /*@requires tainted *s@*/;
+
+void test2 (char **def) /*@requires untainted *def@*/ 
+{
+  checkUntainted (def); 
+  checkTainted (def); /* error */
+}
+
+void test (char *def2) /*@requires untainted def2@*/ 
+{
+  checkUntainted1 (&def2); 
+  checkTainted1 (&def2); /* error */
+}
+
diff --git a/test/tainted/test.c b/test/tainted/test.c
new file mode 100644
index 0000000..9060081
--- /dev/null
+++ b/test/tainted/test.c
@@ -0,0 +1,8 @@
+void test (/*@tainted@*/ char *s)
+{
+  char *t = malloc (sizeof (char) * strlen (s));
+  assert (t != NULL);
+  strcpy (t, s);
+  /* t is tainted too */
+  (void) system (t); /* error */
+}