Fixed test annotations

marcoeilers · Aug 22, 2023 · 0af0a45 · 0af0a45
1 parent 90d9422
commit 0af0a45
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 12 deletions.
diff --git a/tests/functional/verification/issues/00024.py b/tests/functional/verification/issues/00024.py
diff --git a/tests/functional/verification/issues/00074.py b/tests/functional/verification/issues/00074.py
@@ -7,15 +7,15 @@
 
 class Super:
 
-    #:: Label(L1)
     def foo(self, *args: Tuple[int]) -> int:
         Requires(len(args) > 3)
+        #:: ExpectedOutput(postcondition.violated:assertion.false,L1)
         Ensures(Result() > 2)
         return 5
 
-    #:: Label(L2)
     def bar(self, **kwargs: Dict[str, int]) -> int:
         Requires(len(kwargs) > 3)
+        #:: ExpectedOutput(postcondition.violated:assertion.false,L2)
         Ensures(Result() > 2)
         return 5
 
@@ -35,14 +35,14 @@ def bar(self, **kwargs: Dict[str, int]) -> int:
 
 class Sub2(Super):
 
+    #:: Label(L1)
     def foo(self, *args: Tuple[int]) -> int:
         Requires(len(args) > 2)
-        #:: ExpectedOutput(postcondition.violated:assertion.false,L1)
         Ensures(Result() > 0)
         return 5
 
+    #:: Label(L2)
     def bar(self, **kwargs: Dict[str, int]) -> int:
         Requires(len(kwargs) > 2)
-        #:: ExpectedOutput(postcondition.violated:assertion.false,L2)
         Ensures(Result() > 0)
         return 5
diff --git a/tests/functional/verification/issues/00150.py b/tests/functional/verification/issues/00150.py
@@ -21,7 +21,7 @@ def can_node_be_compressed(marked_execution_tree: 'Node') -> int:
     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)
+    #:: ExpectedOutput(postcondition.violated:assertion.false)
     Ensures(Implies(len(marked_execution_tree.children) != 1, Result() == 0))
     Ensures(Result() == 0)
     if len(marked_execution_tree.children) != 1: