*** empty log message ***

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

diff --git a/test/mergestate/tainted.mts b/test/mergestate/tainted.mts
new file mode 100644 (file)
index 0000000..4878c11
--- /dev/null
+++ b/test/mergestate/tainted.mts
@@ -0,0 +1,21 @@
+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
+   defaults 
+      reference ==> tainted
+      parameter ==> tainted
+      result ==> tainted
+      literal ==> untainted
+      null ==> untainted 
+end
+
+
+