Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: Check well-definedness of forall-ensures #2606

Merged
merged 4 commits into from
Aug 19, 2022
Merged

fix: Check well-definedness of forall-ensures #2606

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2dae005
fix: Check well-definedness of forall-ensures
RustanLeino Aug 17, 2022
ad59a9c
Update PR number in release notes
RustanLeino Aug 17, 2022
6f25adb
Merge branch 'master' into issue-2605
RustanLeino Aug 17, 2022
dde7d5d
Merge branch 'master' into issue-2605
keyboardDrummer Aug 19, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions RELEASE_NOTES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
(https://github.com/dafny-lang/dafny/pull/2522)
- feat: `predicate P(x: int): (y: bool) ...` is now valid syntax (https://github.com/dafny-lang/dafny/pull/2454)
- fix: Improve the performance of proofs involving bit vector shifts (https://github.com/dafny-lang/dafny/pull/2520)
- fix: Perform well-definedness checks for ensures clauses of forall statements (https://github.com/dafny-lang/dafny/pull/2606)

# 3.7.3

Expand Down
12 changes: 9 additions & 3 deletions Source/Dafny/Verifier/Translator.TrStatement.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -993,9 +993,9 @@ void TrForallProof(ForallStmt s, BoogieStmtListBuilder definedness, BoogieStmtLi
// havoc x,y;
// CheckWellformed( Range );
// assume Range(x,y);
// Tr( Body );
// CheckWellformed( Post );
// assert Post;
// Tr( Body ); // include only if there is a Body
// assert Post; // include only if there is a Body
// assume false;
// } else {
// assume (forall x,y :: Range(x,y) ==> Post(x,y));
Expand All @@ -1022,12 +1022,18 @@ void TrForallProof(ForallStmt s, BoogieStmtListBuilder definedness, BoogieStmtLi
TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false);
definedness.Add(TrAssumeCmd(s.Range.tok, etran.TrExpr(s.Range)));

var ensuresDefinedness = new BoogieStmtListBuilder(this);
foreach (var ens in s.Ens) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd prefer longer variable names: ensures[Clause] in this case.

TrStmt_CheckWellformed(ens.E, ensuresDefinedness, locals, etran, false);
ensuresDefinedness.Add(TrAssumeCmd(ens.E.tok, etran.TrExpr(ens.E)));
}
PathAsideBlock(s.Tok, ensuresDefinedness, definedness);

if (s.Body != null) {
TrStmt(s.Body, definedness, locals, etran);

// check that postconditions hold
foreach (var ens in s.Ens) {

bool splitHappened; // we actually don't care
foreach (var split in TrSplitExpr(ens.E, etran, true, out splitHappened)) {
if (split.IsChecked) {
Expand Down
12 changes: 12 additions & 0 deletions Test/git-issues/git-issue-2605.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// RUN: %dafny_0 /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

method M(a: array<int>, j: int) {
forall n | 0 <= n < 100
ensures n / 0 == n / 0 // error (x2): division by zero
ensures a[j] == a[j] // error (x2): array index out of bounds
{
assert false; // error
}
assert false; // error
}
7 changes: 7 additions & 0 deletions Test/git-issues/git-issue-2605.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
git-issue-2605.dfy(6,14): Error: possible division by zero
git-issue-2605.dfy(6,23): Error: possible division by zero
git-issue-2605.dfy(7,13): Error: index out of range
git-issue-2605.dfy(7,21): Error: index out of range
git-issue-2605.dfy(9,11): Error: assertion might not hold

Dafny program verifier finished with 0 verified, 5 errors