From 6d1d00069cb6bc0827c07e28306a25689fb031f8 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 27 May 2024 21:48:19 +0200 Subject: [PATCH 1/2] Adding error messages for fold/unfold with non-positive permission, fixing a crash --- src/nagini_translation/lib/errors/messages.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/nagini_translation/lib/errors/messages.py b/src/nagini_translation/lib/errors/messages.py index 74220a5d..87a15e82 100644 --- a/src/nagini_translation/lib/errors/messages.py +++ b/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.', From 76ae221ec1a25a392682d3aa793f4dff43db5b12 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 27 May 2024 21:49:56 +0200 Subject: [PATCH 2/2] Extended test --- tests/functional/verification/test_predicate.py | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/tests/functional/verification/test_predicate.py b/tests/functional/verification/test_predicate.py index f302a0f7..63243cc0 100644 --- a/tests/functional/verification/test_predicate.py +++ b/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) \ No newline at end of file + 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))