Merge pull request #177 from marcoeilers/fix_176

Fixing #176

src/nagini_translation/translators/call.py

@@ -957,16 +957,17 @@ def _inline_call(self, method: PythonMethod, node: ast.Call, is_super: bool,
         if method in ctx.inlined_calls:
             raise InvalidProgramException(node, 'recursive.static.call')
         position = self.to_position(node, ctx)
-        old_position = ctx.position
         ctx.position.append((inline_reason, position))
         arg_stmts, arg_vals, arg_types = self._translate_call_args(node, ctx)
         args = []
         stmts = arg_stmts
 
         # Create local vars for parameters and assign args to them
         if is_super:
-            arg_vals = ([next(iter(ctx.actual_function.args.values())).ref()] +
-                        arg_vals)
+            self_var_name = next(iter(ctx.actual_function.args.keys()))
+            self_var = (ctx.var_aliases[self_var_name] if self_var_name in ctx.var_aliases
+                        else next(iter(ctx.actual_function.args.values())))
+            arg_vals = [self_var.ref()] + arg_vals
         for arg_val, (_, arg) in zip(arg_vals, method.args.items()):
             arg_var = ctx.current_function.create_variable('arg', arg.type,
                                                            self.translator)

tests/functional/verification/issues/00176.py

@@ -0,0 +1,34 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+from nagini_contracts.contracts import *
+
+
+class Grandparent:
+    def __init__(sef) -> None:
+        sef.x = 1
+        Ensures(Acc(sef.x))
+        Ensures(sef.x == 1)
+
+
+class Parent(Grandparent):
+    def __init__(seelf) -> None:
+        super().__init__()
+        Ensures(Acc(seelf.x))
+        Ensures(seelf.x == 1)
+
+
+class Child(Parent):
+    def __init__(self) -> None:
+        super().__init__()
+        Ensures(Acc(self.x))
+        Ensures(self.x == 1)
+
+
+def main() -> None:
+    c = Child()
+    Assert(c.x == 1)
+
+
+if __name__ == "__main__":
+    main()