*** empty log message ***

[splint.git] / test / tainted / tainted.mts

diff --git a/test/tainted/tainted.mts b/test/tainted/tainted.mts
new file mode 100644 (file)
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
+
+
+