Added source references and copyright headers

tests/sif-poss/verification/examples/cav2021-fig9.py

@@ -1,3 +1,6 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
 from nagini_contracts.contracts import *
 from nagini_contracts.lock import Lock
 from nagini_contracts.obligations import Level, WaitLevel

tests/sif-poss/verification/examples/no_obligations/cav2021-fig11.py

@@ -1,6 +1,12 @@
 # Any copyright is dedicated to the Public Domain.
 # http://creativecommons.org/publicdomain/zero/1.0/
 
+"""
+Example adapted from "Principles of Secure Information Flow Analysis"
+G. Smith
+Malware Detection, 2007
+"""
+
 from nagini_contracts.contracts import *
 from nagini_contracts.lock import Lock
 from nagini_contracts.obligations import WaitLevel, Level, MustRelease

tests/sif-prob/verification/examples/no_obligations/cav2021-fig9.py

@@ -1,3 +1,6 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
 from nagini_contracts.contracts import *
 from nagini_contracts.lock import Lock
 

tests/sif-prob/verification/examples/no_obligations/secc-cav2019.py

@@ -1,3 +1,13 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+"""
+Example adapted from "SecCSL: Security Concurrent Separation Logic"
+G. Ernst and T. Murray
+CAV 2019
+https://bitbucket.org/covern/secc/src/master/examples/case-studies/
+"""
+
 from nagini_contracts.contracts import *
 from nagini_contracts.lock import Lock
 

tests/sif-prob/verification/examples/no_obligations/secc-cddc.py

@@ -1,3 +1,10 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+"""
+Example adapted from https://bitbucket.org/covern/secc/src/master/examples/case-studies/
+"""
+
 #:: IgnoreFile(carbon)(107)
 
 from nagini_contracts.adt import ADT

tests/sif-prob/verification/examples/no_obligations/secc-ct.py

@@ -1,3 +1,10 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+"""
+Example adapted from https://bitbucket.org/covern/secc/src/master/examples/case-studies/
+"""
+
 from nagini_contracts.contracts import *
 from typing import List
 

tests/sif-true/verification/examples/no_obligations/secc-db.py

@@ -1,6 +1,10 @@
 # Any copyright is dedicated to the Public Domain.
 # http://creativecommons.org/publicdomain/zero/1.0/
 
+"""
+Example adapted from https://bitbucket.org/covern/secc/src/master/examples/case-studies/
+"""
+
 from nagini_contracts.contracts import *
 from typing import List, Tuple
 

tests/sif-true/verification/examples/no_obligations/secc-encrypt.py

@@ -1,6 +1,10 @@
 # Any copyright is dedicated to the Public Domain.
 # http://creativecommons.org/publicdomain/zero/1.0/
 
+"""
+Example adapted from https://bitbucket.org/covern/secc/src/master/examples/case-studies/
+"""
+
 from nagini_contracts.contracts import *
 from typing import List