diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index 3763ddfd4dd..f2144918121 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/Source/DafnyCore/AST/Tokens.cs @@ -66,6 +66,7 @@ public Token(int linenum, int colnum) { this.val = ""; } + public bool IsSourceToken => this != NoToken; public int kind { get; set; } // Used by coco, so we can't rename it to Kind public string ActualFilename => Filepath; @@ -160,6 +161,8 @@ public bool IsValid { get { return WrappedToken.IsValid; } } + public virtual bool IsSourceToken => false; + public int kind { get { return WrappedToken.kind; } set { WrappedToken.kind = value; } @@ -305,6 +308,8 @@ public override IToken WithVal(string newVal) { throw new NotImplementedException(); } + public override bool IsSourceToken => this != NoToken; + public BoogieRangeToken ToToken() { return new BoogieRangeToken(StartToken, EndToken, null); } diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 7aaae0f4f65..6c65a128f29 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -34,7 +34,7 @@ - + diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 3787e5d1eac..0daff1c5f67 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -198,7 +198,7 @@ string OriginDescription(IImplementationPartOrigin origin, bool outer) { var result = origin switch { PathOrigin pathOrigin => $"{OriginDescription(pathOrigin.Inner, false)}" + $"after executing lines {string.Join(", ", pathOrigin.BranchTokens.Select(b => b.line))}", - RemainingAssertionsOrigin remainingAssertions => $"{OriginDescription(remainingAssertions.Origin, false)}remaining assertions", + RemainingAssertionsOrigin remainingAssertions => OriginDescription(remainingAssertions.Origin, false) + (outer ? "remaining assertions" : ""), IsolatedAssertionOrigin isolateOrigin => $"{OriginDescription(isolateOrigin.Origin, false)}assertion at line {isolateOrigin.line}", JumpOrigin returnOrigin => $"{OriginDescription(returnOrigin.Origin, false)}{JumpOriginKind(returnOrigin)} at line {returnOrigin.line}", AfterSplitOrigin splitOrigin => $"{OriginDescription(splitOrigin.Inner, false)}assertions after split_here at line {splitOrigin.line}", diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy index fb7ceac5f26..34ab6377f30 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy @@ -1,9 +1,9 @@ // RUN: ! %verify --isolate-assertions --cores=1 --progress VerificationJobs "%s" &> %t.raw // RUN: %sed 's#\(time.*\)##g' %t.raw > %t // RUN: %diff "%s.expect" "%t" - -ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)} - +ghost function f(i:nat, j:nat):int { + if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j) +} lemma{:resource_limit 10000000} L() { assert true; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy index f53d0332b77..2363f8d4aca 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy @@ -1,13 +1,19 @@ -// RUN: %verify --progress VerificationJobs --cores=1 %s &> %t.raw +// RUN: ! %verify --progress VerificationJobs --cores=1 %s &> %t.raw // RUN: %sed 's#\(time.*\)##g' %t.raw > %t // RUN: %diff "%s.expect" "%t" - - -method {:isolate_assertions} Foo() { +method {:isolate_assertions} Foo(x: int) returns (r: int) + ensures r > 3 + ensures r < 10 +{ assert true; assert true; + if (x == 3) { + return 7; + } else { + return 12; + } } method Bar() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect index ce6205ddf27..9c0187038c8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect @@ -1,7 +1,13 @@ Verified 0/2 symbols. Waiting for Foo to verify. -Verified 1/2 of Foo: assertion at line 9 - verified successfully -Verified 2/2 of Foo: assertion at line 10 - verified successfully +Verified 1/6 of Foo: assertion at line 10 - verified successfully +Verified 2/6 of Foo: assertion at line 11 - verified successfully +Verified 3/6 of Foo: return at line 15, assertion at line 7 - verified successfully +Verified 4/6 of Foo: return at line 15, assertion at line 8 - could not be verified +Verified 5/6 of Foo: return at line 13, assertion at line 7 - verified successfully +Verified 6/6 of Foo: return at line 13, assertion at line 8 - verified successfully +isolateAllAssertions.dfy(15,4): Error: a postcondition could not be proved on this return path +isolateAllAssertions.dfy(8,12): Related location: this is the postcondition that could not be proved Verified 1/2 symbols. Waiting for Bar to verify. Verified 1/1 of Bar: entire body - verified successfully -Dafny program verifier finished with 3 verified, 0 errors +Dafny program verifier finished with 6 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect index e352fc10535..6252fafc31c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 142 verified, 0 errors +Dafny program verifier finished with 148 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect index 3b71b05bfb8..2f021147f08 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 55 verified, 0 errors +Dafny program verifier finished with 67 verified, 0 errors diff --git a/customBoogie.patch b/customBoogie.patch index 67588e2f762..9023f27d395 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + + + diff --git a/docs/dev/news/5917.feat b/docs/dev/news/5917.feat new file mode 100644 index 00000000000..0303609187f --- /dev/null +++ b/docs/dev/news/5917.feat @@ -0,0 +1 @@ +When using `--isolate-assertions` or `{:isolate_assertions}`, a separate assertion batch will be generated per pair of return statement and ensures clause. \ No newline at end of file