--- /dev/null
+
+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
--- /dev/null
+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;
+}
+
--- /dev/null
+
+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
--- /dev/null
+
+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
--- /dev/null
+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)
+
--- /dev/null
+/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
--- /dev/null
+/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
--- /dev/null
+.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
--- /dev/null
+.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
--- /dev/null
+extern char *mtainted (char *s);
+
+void test (/*@untainted@*/ char *s)
+{
+ (void) system (mtainted (s));
+}
--- /dev/null
+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 */
+}
--- /dev/null
+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
+
+
+
--- /dev/null
+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 */
+}
--- /dev/null
+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
+
+
+
--- /dev/null
+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
+
+
+
--- /dev/null
+/*
+** 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)@*/ ;
+
--- /dev/null
+# 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;
+}
--- /dev/null
+extern void checkUntainted (/*@untainted@*/ char *s) ;
+extern void checkTainted (/*@tainted@*/ char *s) ;
+
+void test (/*@tainted@*/ char *def)
+{
+ checkTainted (def);
+ checkUntainted (def); /* error */
+}
--- /dev/null
+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 */
+}
--- /dev/null
+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 */
+}
--- /dev/null
+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 */
+}
--- /dev/null
+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 */
+}
--- /dev/null
+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 */
+}
--- /dev/null
+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 */
+}
--- /dev/null
+char *taintme (char *s)
+ /*@ensures result:taintedness = s:taintedness@*/
+{
+ char *res = (char *) malloc (sizeof (*res) * strlen (s));
+
+ strcpy (res, s);
+ return s;
+}
--- /dev/null
+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 */
+}
--- /dev/null
+char *f (/*@tainted@*/ char *s)
+{
+ char t[50];
+
+ strcpy (t, "test");
+
+ (void) system (t);
+
+ strcat (t, s);
+
+ (void) system (t); /* error */
+}
--- /dev/null
+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 */
+}
+
--- /dev/null
+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 */
+}