Skip to content

Commit

Permalink
Merge branch 'master' into chore-do-boogie-translation
Browse files Browse the repository at this point in the history
  • Loading branch information
MikaelMayer committed Jan 23, 2025
2 parents 2e5d2c8 + bf9cf16 commit 61a457f
Showing 6 changed files with 23 additions and 9 deletions.
9 changes: 3 additions & 6 deletions Source/DafnyCore/Dafny.atg
Original file line number Diff line number Diff line change
@@ -2391,19 +2391,16 @@ AssignStatement<out Statement/*!*/ s>
s = new AssignSuchThatStmt(rangeToken, lhss, suchThat, suchThatAssume, null);
} else if (exceptionRhs != null) {
s = new AssignOrReturnStmt(rangeToken, lhss, exceptionRhs, keywordToken, rhss);
if (proof != null) {
s = new BlockByProofStmt(rangeToken, proof, s);
}
} else {
if (lhss.Count == 0 && rhss.Count == 0) {
s = new BlockStmt(rangeToken, new List<Statement>()); // error, give empty statement
} else {
s = new AssignStatement(rangeToken, lhss, rhss);
if (proof != null) {
s = new BlockByProofStmt(rangeToken, proof, s);
}
}
}
if (proof != null) {
s = new BlockByProofStmt(rangeToken, proof, s);
}
.)
.

8 changes: 8 additions & 0 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md
Original file line number Diff line number Diff line change
@@ -68,6 +68,14 @@ will be flagged by CI, and should be fixed by either converting it to use
to flag it as intentionally inconsistent,
for tests of backend-specific externs for example.

If a platform is not supported, please use the following command:

```
// UNSUPPORTED: windows, macosx
```

You can specify one or multiple platforms separated by a comma among `windows`, `posix`, `macosx`

## Executing Tests from JetBrains Rider

You will likely find it more convenient to run tests from an IDE such as
Original file line number Diff line number Diff line change
@@ -5,4 +5,12 @@ method ByClause(b: bool) {
var r: int :| false by {
assume {:axiom} false;
}
}

function F(x: int): int
method ByClauseSeparateAssignment() {
var a;
a :| F(a) == 2 by {
assume {:axiom} F(10) == 2;
}
}
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@

Dafny program verifier finished with 1 verified, 0 errors
Dafny program verifier finished with 2 verified, 0 errors
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// UNSUPPORTED: macosx
// Unsupported because the resource count is slightly different on macosx
// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation --performance-stats=1


codatatype Stream<T> = Cons(head: T, tail: Stream)

ghost function Upward(n: int): Stream<int>
1 change: 1 addition & 0 deletions docs/dev/news/6024.fix
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
By clauses for assign-such-that statements (:|), are now never ignored.

0 comments on commit 61a457f

Please sign in to comment.