Skip to content

Commit

Permalink
Adding test
Browse files Browse the repository at this point in the history
  • Loading branch information
marcoeilers committed Mar 15, 2024
1 parent 9d8f182 commit df2b85c
Showing 1 changed file with 34 additions and 0 deletions.
34 changes: 34 additions & 0 deletions tests/functional/verification/issues/00176.py
Original file line number Diff line number Diff line change
@@ -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()

0 comments on commit df2b85c

Please sign in to comment.