From 2ee4b8487d4c9f3f7cd5773b84bfc82e4eb6d92a Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 22 Jan 2025 12:11:02 +0100 Subject: [PATCH 1/3] Fix CoinductiveProofs.dfy granularity --- .../TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy | 2 +- .../LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy index f89bf98bb9d..8172cf7c70d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation --performance-stats=1 +// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation --performance-stats=10 codatatype Stream = Cons(head: T, tail: Stream) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect index 53fd056694d..e666e590888 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect @@ -31,5 +31,5 @@ CoinductiveProofs.dfy(208,21): Related location: this is the postcondition that CoinductiveProofs.dfy(4,23): Related location: this proposition could not be proved Dafny program verifier finished with 23 verified, 12 errors -Total resources used is 748143 -Max resources used by VC is 59297 +Total resources used is 748150 +Max resources used by VC is 59300 From 3d0bbe2ece75af36d41134732be1859d2f94c53b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 22 Jan 2025 12:13:42 +0100 Subject: [PATCH 2/3] Add back documentation update --- .../IntegrationTests/TestFiles/LitTests/LitTest/README.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md b/Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md index d630eb72a7b..be1c7db654c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md @@ -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 From 84a870b99d4f26954bd8bcdcc794f51c07f818e2 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 22 Jan 2025 15:07:13 +0100 Subject: [PATCH 3/3] Reduce accuracy further --- .../LitTests/LitTest/ast/statement/opaqueBlock.dfy | 6 ++++++ .../LitTest/ast/statement/opaqueBlock.dfy.expect | 10 ++++++---- .../LitTests/LitTest/dafny0/CoinductiveProofs.dfy | 2 +- .../LitTest/dafny0/CoinductiveProofs.dfy.expect | 2 +- 4 files changed, 14 insertions(+), 6 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy index 8b9e73f15ff..15672db94f4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy @@ -134,6 +134,12 @@ method DefiniteAssignment() } } target := z; + + var q: int; + opaque + ensures q == 3 + { + } } method EnsuresDoesNotHold() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect index c6eaab54b1a..abc13bad8d6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect @@ -9,8 +9,10 @@ opaqueBlock.dfy(93,2): Error: opaque block might violate context's modifies clau opaqueBlock.dfy(106,4): Error: opaque block might violate context's modifies clause opaqueBlock.dfy(127,12): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here opaqueBlock.dfy(130,17): Error: variable 'z', which is subject to definite-assignment rules, might be uninitialized here -opaqueBlock.dfy(142,12): Error: ensures might not hold -opaqueBlock.dfy(206,6): Error: assignment might update an object not in the enclosing context's modifies clause -opaqueBlock.dfy(218,2): Error: assertion might not hold +opaqueBlock.dfy(140,12): Error: variable 'q', which is subject to definite-assignment rules, might be uninitialized here +opaqueBlock.dfy(140,14): Error: ensures might not hold +opaqueBlock.dfy(148,12): Error: ensures might not hold +opaqueBlock.dfy(212,6): Error: assignment might update an object not in the enclosing context's modifies clause +opaqueBlock.dfy(224,2): Error: assertion might not hold -Dafny program verifier finished with 3 verified, 14 errors +Dafny program verifier finished with 3 verified, 16 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy index 8172cf7c70d..cd9d5e3beaf 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation --performance-stats=10 +// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation --performance-stats=100 codatatype Stream = Cons(head: T, tail: Stream) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect index e666e590888..d8c16264353 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect @@ -31,5 +31,5 @@ CoinductiveProofs.dfy(208,21): Related location: this is the postcondition that CoinductiveProofs.dfy(4,23): Related location: this proposition could not be proved Dafny program verifier finished with 23 verified, 12 errors -Total resources used is 748150 +Total resources used is 748100 Max resources used by VC is 59300