Merge pull request #193 from marcoeilers/non_positive_fold

Add error message for fold/unfold with non-positive permissions

src/nagini_translation/lib/errors/messages.py

@@ -99,6 +99,8 @@
         lambda n: 'Divisor {} might be zero.'.format(pprint(n)),
     'negative.permission':
         lambda n: 'Fraction {} might be negative.'.format(pprint(n)),
+    'permission.not.positive':
+        lambda n: 'Fraction {} might not be positive'.format(pprint(n)),
     'insufficient.permission':
         lambda n: ('There might be insufficient permission to '
                    'access {}.').format(pprint(n)),
@@ -203,6 +205,7 @@
     'receiver.null': 'Receiver might be null.',
     'division.by.zero': 'Divisor might be zero.',
     'negative.permission': 'Fraction might be negative.',
+    'permission.not.positive': 'Fraction might not be positive.',
     'insufficient.permission': 'There might be insufficient permission.',
     'termination_measure.non_positive': 'Termination measure might be non-positive.',
     'measure.non_decreasing': 'Termination measure might not be smaller.',

tests/functional/verification/test_predicate.py

@@ -66,4 +66,14 @@ def main_6() -> int:
     s = Super(34, 99)
     Fold(other_pred(s))
     #:: ExpectedOutput(assignment.failed:insufficient.permission)
-    return Unfolding(some_pred(s, 34, 34), s.field3)
+    return Unfolding(some_pred(s, 34, 34), s.field3)
+
+
+@Predicate
+def pure(i: int) -> bool:
+    return i > 0
+
+
+def previously_unsound() -> None:
+    #:: ExpectedOutput(unfold.failed:permission.not.positive)
+    Unfold(Acc(pure(-5), 0/1))