Tests for old issues and some small fixes

src/nagini_translation/resources/preamble.index

@@ -542,7 +542,8 @@
         },
         "__len__": {
             "args": ["tuple"],
-            "type": "__prim__int"
+            "type": "__prim__int",
+            "requires": ["__val__", "args"]
         },
         "__val__": {
             "args": ["tuple"],

src/nagini_translation/translators/program.py

@@ -296,6 +296,13 @@ def create_override_check(self, method: PythonMethod,
             params.append(method.overrides.args[arg].decl)
             args.append(method.overrides.args[arg].ref())
 
+        if method.overrides.var_arg:
+            params.append(method.overrides.var_arg.decl)
+            args.append(method.overrides.var_arg.ref())
+        if method.overrides.kw_arg:
+            params.append(method.overrides.kw_arg.decl)
+            args.append(method.overrides.kw_arg.ref())
+
         self.bind_type_vars(method.overrides, ctx)
 
         mname = ctx.module.get_fresh_name(method.sil_name + '_override_check')

tests/functional/verification/issues/00024.py

@@ -0,0 +1,7 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+
+def bla() -> None:
+    #:: ExpectedOutput(type.error:Cannot resolve name "a" (possible cyclic definition))
+    a = a

tests/functional/verification/issues/00052.py

@@ -0,0 +1,62 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+
+from nagini_contracts.contracts import (
+    Acc,
+    Assert,
+    Requires,
+    Invariant,
+    Implies,
+    Predicate,
+    Fold,
+    Ensures,
+    Unfold,
+    Unfolding,
+)
+from nagini_contracts.obligations import *
+
+
+class Tree:
+
+    @Predicate
+    def valid(self) -> bool:
+        return (Acc(self.left) and Acc(self.right) and
+                Acc(self.height, 1/10) and self.height >= 0 and
+                Implies(
+                    self.left is not None,
+                    self.left.valid() and Acc(self.left.height, 1/10) and
+                    self.left.height == self.height - 1) and
+                Implies(
+                    self.right is not None,
+                    self.right.valid() and Acc(self.right.height, 1/10) and
+                    self.right.height == self.height - 1)
+                )
+
+    def __init__(self, left: 'Tree', right: 'Tree', height: int) -> None:
+        Requires(left.valid() and Acc(left.height, 1/10) and
+                 left.height == height-1)
+        Requires(right.valid() and Acc(right.height, 1/10) and
+                 right.height == height-1)
+        Requires(height >= 0)
+        Ensures(self.valid())
+        self.left = left        # type: Tree
+        self.right = right      # type: Tree
+        self.height = height    # type: int
+        Fold(self.valid())
+
+
+    def work(self, call_height: int) -> None:
+        Requires(self.valid())
+        Requires(call_height >= 0)
+        Requires(Unfolding(self.valid(), self.height == call_height))
+        Requires(MustTerminate(call_height + 1))
+        Ensures(self.valid())
+
+        if call_height > 0:
+            Unfold(self.valid())
+            if self.left is not None:
+                self.left.work(call_height - 1)
+            if self.right is not None:
+                self.right.work(call_height - 1)
+            Fold(self.valid())

tests/functional/verification/issues/00074.py

@@ -0,0 +1,48 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+
+from typing import Tuple, Dict
+from nagini_contracts.contracts import Requires, Ensures, Result
+
+class Super:
+
+    #:: Label(L1)
+    def foo(self, *args: Tuple[int]) -> int:
+        Requires(len(args) > 3)
+        Ensures(Result() > 2)
+        return 5
+
+    #:: Label(L2)
+    def bar(self, **kwargs: Dict[str, int]) -> int:
+        Requires(len(kwargs) > 3)
+        Ensures(Result() > 2)
+        return 5
+
+
+class Sub(Super):
+
+    def foo(self, *args: Tuple[int]) -> int:
+        Requires(len(args) > 2)
+        Ensures(Result() > 4)
+        return 5
+
+    def bar(self, **kwargs: Dict[str, int]) -> int:
+        Requires(len(kwargs) > 2)
+        Ensures(Result() > 4)
+        return 5
+
+
+class Sub2(Super):
+
+    def foo(self, *args: Tuple[int]) -> int:
+        Requires(len(args) > 2)
+        #:: ExpectedOutput(postcondition.violated:assertion.false,L1)
+        Ensures(Result() > 0)
+        return 5
+
+    def bar(self, **kwargs: Dict[str, int]) -> int:
+        Requires(len(kwargs) > 2)
+        #:: ExpectedOutput(postcondition.violated:assertion.false,L2)
+        Ensures(Result() > 0)
+        return 5

tests/functional/verification/issues/00119.py

@@ -0,0 +1,18 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+from nagini_contracts.contracts import *
+
+class A:
+    def __init__(self, value: int) -> None:
+        self.value = value  # type: int
+        Ensures(Acc(self.value) and self.value is value)
+
+
+def test() -> None:
+    Assert(A(5).value == 5)
+
+
+def test2() -> None:
+    #:: ExpectedOutput(assert.failed:assertion.false)
+    Assert(A(3).value == 5)

tests/functional/verification/issues/00150.py

@@ -0,0 +1,31 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+
+from typing import Optional, List, Tuple
+from nagini_contracts.contracts import *
+
+class Node:
+    def __init__(self, function_name: str, children:List['Node']) -> None:
+        self.function_name = function_name # type: str
+        self.children = children # type: List['Node']
+        Ensures(Acc(self.function_name) and self.function_name is function_name and
+                Acc(self.children) and self.children is children)
+
+@Pure
+def can_node_be_compressed(marked_execution_tree: 'Node') -> int:
+    """Searches for the longest compression possible. Returns:
+    - int: number of nodes that can be compressed. 0 if None"""
+    Requires(Acc(marked_execution_tree.children))
+    Requires(Acc(list_pred(marked_execution_tree.children)))
+    Requires(Forall(int, lambda i: Implies(i >= 0 and i < len(marked_execution_tree.children),
+                                           Acc(marked_execution_tree.children[i].function_name))))
+    Requires(Acc(marked_execution_tree.function_name))
+    #:: ExpectedOutput(postcondition.violdated:assertion.false)
+    Ensures(Implies(len(marked_execution_tree.children) != 1, Result() == 0))
+    Ensures(Result() == 0)
+    if len(marked_execution_tree.children) != 1:
+        return 1
+    if marked_execution_tree.children[0].function_name != marked_execution_tree.function_name:
+        return 0
+    return can_node_be_compressed(marked_execution_tree.children[0]) + 1