tainted.c: (in function f)
tainted.c:5:20: Invalid transfer from tainted s to untainted (Possibly tainted
- storage used as untainted.): s
- tainted.c:3:48: Meta state s becomes tainted
+ storage used as untainted.): f(..., s, ...)
+ tainted.c:3:48: s becomes tainted
+ tainted.c:3:74: us becomes untainted
tainted.c: (in function test)
tainted.c:12:18: Invalid transfer from tainted s to untainted (Possibly tainted
- storage used as untainted.): s
- tainted.c:9:34: Meta state s becomes tainted
+ storage used as untainted.): system(..., s, ...)
+ tainted.c:9:34: s becomes tainted
+ tainted.xh:26:55: s becomes untainted
tainted.c:17:18: Invalid transfer from tainted t to untainted (Possibly tainted
- storage used as untainted.): t
- tainted.c:15:3: Meta state t becomes tainted
+ storage used as untainted.): system(..., t, ...)
+ tainted.c:15:3: t becomes tainted
+ tainted.xh:26:55: s becomes untainted
tainted.c:20:18: Invalid transfer from tainted t to untainted (Possibly tainted
- storage used as untainted.): t
- tainted.c:19:3: Meta state t becomes tainted
+ storage used as untainted.): system(..., t, ...)
+ tainted.c:19:3: t becomes tainted
+ tainted.xh:26:55: s becomes untainted
-Finished LCLint checking --- 4 code errors found, as expected
+Finished checking --- 4 code warnings, as expected
tainted-bad.mts:18:7: Transfer clause uses unrecognized result state peach:
untainted as tainted ==> peach
maybetainted reference ==> blue
tainted-bad.mts:5:21: Defaults declaration uses unrecognized value name
stainted: stainted reference
-tainted-bad.mts:7:21: Duplicate defaults declaration for context param:
- untainted param
+tainted-bad.mts:7:21: Duplicate defaults declaration for context parameter:
+ untainted parameter
tainted.c: (in function f)
tainted.c:5:20: Invalid transfer from tainted s to untainted (Possibly tainted
- storage used as untainted.): s
- tainted.c:3:48: Meta state s becomes tainted
+ storage used as untainted.): f(..., s, ...)
+ tainted.c:3:48: s becomes tainted
+ tainted.c:3:74: us becomes untainted
tainted.c: (in function test)
tainted.c:12:18: Invalid transfer from tainted s to untainted (Possibly tainted
- storage used as untainted.): s
- tainted.c:9:34: Meta state s becomes tainted
+ storage used as untainted.): system(..., s, ...)
+ tainted.c:9:34: s becomes tainted
+ tainted.xh:26:55: s becomes untainted
tainted.c:17:18: Invalid transfer from tainted t to untainted (Possibly tainted
- storage used as untainted.): t
- tainted.c:15:3: Meta state t becomes tainted
+ storage used as untainted.): system(..., t, ...)
+ tainted.c:15:3: t becomes tainted
+ tainted.xh:26:55: s becomes untainted
tainted.c:20:18: Invalid transfer from tainted t to untainted (Possibly tainted
- storage used as untainted.): t
- tainted.c:15:3: Meta state t becomes tainted
+ storage used as untainted.): system(..., t, ...)
+ tainted.c:15:3: t becomes tainted
+ tainted.xh:26:55: s becomes untainted
-Finished LCLint checking --- 9 code errors found, as expected
+Finished checking --- 9 code warnings, as expected
tainted2.c: (in function test)
-tainted2.c:18:5: Control branches merge with incompatible states for stk
- (untainted and tainted): Incompatible state merge (default behavior)
- tainted2.c:17:14: Meta state stk becomes tainted
- tainted2.c:11:7: Meta state stk becomes untainted
+tainted2.c:20:10: Invalid transfer from tainted stk to untainted (Possibly
+ tainted storage used as untainted.): return stk
+ tainted2.c:17:14: stk becomes tainted
+ tainted2.c:4:2: becomes untainted
-Finished LCLint checking --- 1 code error found, as expected
+Finished checking --- 1 code warning, as expected
tainted3.c: (in function test)
-tainted3.c:7:3: Requires clause of called function checkUntainted not satisfied
- by def (state is tainted): requires untainted def
+tainted3.c:7:19: Invalid transfer from tainted def to untainted (Possibly
+ tainted storage used as untainted.): checkUntainted(..., def, ...)
+ tainted3.c:4:36: def becomes tainted
+ tainted3.c:1:53: def becomes untainted
-Finished LCLint checking --- 1 code error found, as expected
+Finished checking --- 1 code warning, as expected
tainted4.c: (in function test)
-tainted4.c:7:3: Requires clause of called function checkUntainted not satisfied
- by def (state is tainted): requires untainted *def
+tainted4.c:9:19: Invalid transfer from tainted def to untainted (*def):
+ Possibly tainted storage used as untainted.
+ tainted4.c:6:36: def becomes tainted
-Finished LCLint checking --- 1 code error found, as expected
+Finished checking --- 1 code warning, as expected
-tainted5.c: (in function test)
-tainted5.c:7:3: Requires clause of called function checkTainted not satisfied
- by def (state is untainted): requires tainted *def
-tainted5.c: (in function test2)
-tainted5.c:13:3: Requires clause of called function checkTainted not satisfied
- by *def (state is untainted): requires tainted *def
+Finished checking --- no warnings
-Finished LCLint checking --- 2 code errors found, as expected
+taintedmerge.c: (in function f)
+taintedmerge.c:11:18: Invalid transfer from tainted t to untainted (Possibly
+ tainted storage used as untainted.): system(..., t, ...)
+ taintedmerge.c:10:3: t becomes tainted
+ tainted.xh:26:55: s becomes untainted
+taintedmerge.c:14:18: Invalid transfer from tainted t to untainted (Possibly
+ tainted storage used as untainted.): system(..., t, ...)
+ taintedmerge.c:13:3: t becomes tainted
+ tainted.xh:26:55: s becomes untainted
+taintedmerge.c:16:10: Stack-allocated storage t reachable from return value: t
+
+Finished checking --- 3 code warnings, as expected
+
+taintedimplicit.c: (in function dangerouscall)
+taintedimplicit.c:17:18: Invalid transfer from tainted [result of taintme] to
+ untainted (Possibly tainted storage used as untainted.):
+ system(..., taintme(s), ...)
+ taintedimplicit.c:17:18: becomes tainted
+ tainted.xh:26:55: s becomes untainted
+
+Finished checking --- 1 code warning, as expected
+
+sprintf.c: (in function sp)
+sprintf.c:11:18: Invalid transfer from tainted s to untainted (Possibly tainted
+ storage used as untainted.): system(..., s, ...)
+ sprintf.c:10:37: s becomes tainted
+ tainted.xh:26:55: s1 becomes untainted
+sprintf.c:14:18: Invalid transfer from tainted s to untainted (Possibly tainted
+ storage used as untainted.): system(..., s, ...)
+ sprintf.c:13:61: s becomes tainted
+ tainted.xh:26:55: s1 becomes untainted
+
+Finished checking --- 2 code warnings, as expected
andersk / splint.git / blobdiff