Merge pull request #162 from marcoeilers/fix_161

Correctly tracking assignments to static fields

src/nagini_translation/analyzer.py

@@ -1072,6 +1072,7 @@ def todo():
                     # (non-static) field, and created the field. We remove it
                     # again now that we now it's actually static.
                     del self.current_class.fields[node.id]
+                self.track_access(node, var)
                 return
         # We're in a function
         if isinstance(node.ctx, ast.Store):

src/nagini_translation/translators/statement.py

@@ -1097,6 +1097,8 @@ def _assign_single_value(self, lhs: ast.AST, rhs: Expr, rhs_type: PythonType,
         after_assign = []
         if isinstance(target, PythonGlobalVar):
             if target.is_final:
+                if lhs not in target.writes:
+                    raise UnsupportedException(lhs, "Internal error: Variable may have been incorrectly tagged as final.")
                 # For final variables, we assume that the function representing the
                 # variable is equal to the RHS of the assignment. For pure values,
                 # this will do nothing, since the postcondition will already say the same;

tests/functional/verification/issues/00161.py

@@ -0,0 +1,23 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+from nagini_contracts.contracts import *
+
+class Parent:
+    x = 100
+
+
+class Subclass:
+    y = 200
+
+    def __init__(self) -> None:
+        self.x = 100
+        Ensures(Acc(self.x))
+
+
+def main() -> None:
+    instance = Subclass()
+    #:: ExpectedOutput(assert.failed:insufficient.permission)
+    Assert(instance.y == 200)
+    Subclass.y = 300
+    Assert(instance.y == 200)