Fix: Wording of assertion failure closer to semantics #3324
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -7233,7 +7233,7 @@ Bpl.Ensures Ensures(IToken tok, bool free, Bpl.Expr condition, string errorMessa | |
| Contract.Ensures(Contract.Result<Bpl.Ensures>() != null); | ||
|
|
||
| Bpl.Ensures ens = new Bpl.Ensures(ForceCheckToken.Unwrap(tok), free, condition, comment); | ||
| ens.Description = new PODesc.AssertStatement(errorMessage ?? "This is the postcondition that could not be proven."); | ||
| return ens; | ||
| } | ||
|
|
||
|
|
@@ -7242,7 +7242,7 @@ Bpl.Requires Requires(IToken tok, bool free, Bpl.Expr condition, string errorMes | |
| Contract.Requires(condition != null); | ||
| Contract.Ensures(Contract.Result<Bpl.Requires>() != null); | ||
| Bpl.Requires req = new Bpl.Requires(ForceCheckToken.Unwrap(tok), free, condition, comment); | ||
| req.Description = new PODesc.AssertStatement(errorMessage ?? "This is the precondition that could not be proven."); | ||
| return req; | ||
| } | ||
|
|
||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -48,20 +48,20 @@ method Abs(x: int) returns (y: int) | |
| ", "testFile.dfy"); | ||
| // When hovering the postcondition, it should display the position of the failing path | ||
| await AssertHoverMatches(documentItem, (2, 15), | ||
| @"[**Error:**](???) Could not prove this postcondition on a return path. | ||
| This is assertion #1 of 4 in method Abs | ||
| Resource usage: ??? RU | ||
| Return path: testFile.dfy(6, 5)" | ||
| ); | ||
| // When hovering the failing path, it does not display the position of the failing postcondition | ||
| // because the IDE extension already does it. | ||
| await AssertHoverMatches(documentItem, (5, 4), | ||
| @"[**Error:**](???) Could not prove a postcondition on this return path. | ||
| This is assertion #1 of 4 in method Abs | ||
| Resource usage: ??? RU" | ||
| ); | ||
| await AssertHoverMatches(documentItem, (7, 11), | ||
| @"[**Error:**](???) Could not prove assertion | ||
| This is assertion #2 of 4 in method Abs | ||
| Resource usage: 9K RU" | ||
| ); | ||
|
|
@@ -86,7 +86,7 @@ await SetUp(o => { | |
| } | ||
| ", "testfile.dfy"); | ||
| await AssertHoverMatches(documentItem, (1, 12), | ||
| @"[**Error:**](???) Could not prove assertion | ||
| This is the only assertion in [batch](???) #??? of ??? in method f | ||
| [Batch](???) #??? resource usage: ??? RU" | ||
| ); | ||
|
|
@@ -123,7 +123,7 @@ await AssertHoverMatches(documentItem, (2, 12), | |
| [Batch](???) #1 resource usage: ??? RU" | ||
| ); | ||
| await AssertHoverMatches(documentItem, (3, 26), | ||
| @"[**Error:**](???) Could not prove assertion | ||
| This is assertion #1 of 2 in [batch](???) #2 of 2 in function f | ||
| [Batch](???) #2 resource usage: ??? RU" | ||
| ); | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -341,7 +341,7 @@ decreases y | |
| Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[1].Severity); | ||
| Assert.AreEqual(1, diagnostics[0].RelatedInformation.Count()); | ||
| var relatedInformation = diagnostics[0].RelatedInformation.First(); | ||
| Assert.AreEqual("Could not prove this postcondition: product >= 0", relatedInformation.Message); | ||
| Assert.AreEqual(new Range(new Position(2, 30), new Position(2, 42)), relatedInformation.Location.Range); | ||
| await AssertNoDiagnosticsAreComing(CancellationToken); | ||
| } | ||
|
|
@@ -666,7 +666,7 @@ modifies this | |
| Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity); | ||
| var relatedInformation = diagnostics[0].RelatedInformation.ToArray(); | ||
| Assert.AreEqual(2, relatedInformation.Length); | ||
| Assert.AreEqual("Could not prove this postcondition: Valid()", relatedInformation[0].Message); | ||
| Assert.AreEqual(new Range((14, 16), (14, 23)), relatedInformation[0].Location.Range); | ||
| Assert.AreEqual("Could not prove: b < c", relatedInformation[1].Message); | ||
| Assert.AreEqual(new Range((9, 11), (9, 16)), relatedInformation[1].Location.Range); | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -102,7 +102,7 @@ DidChangeTextDocumentParams MakeChange(int? version, Range range, string text) { | |
| Assert.IsNotNull(document); | ||
| Assert.AreEqual(documentItem.Version + 11, document.Version); | ||
| Assert.AreEqual(1, document.Diagnostics.Count()); | ||
| Assert.AreEqual("Could not prove assertion", document.Diagnostics.First().Message); | ||
| } | ||
|
|
||
| [TestMethod, Timeout(MaxTestExecutionTimeMs)] | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -204,7 +204,7 @@ string GetDescription(Boogie.ProofObligationDescription? description) { | |
| if (currentlyHoveringPostcondition && | ||
| (failureDescription == new PostconditionDescription().FailureDescription || | ||
| failureDescription == new EnsuresDescription().FailureDescription)) { | ||
| failureDescription = "Could not prove this postcondition on a return path."; | ||
| } | ||
| return $"{obsolescence}[**Error:**](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-verification-debugging) " + | ||
| failureDescription; | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -93,7 +93,7 @@ private IEnumerable<DiagnosticRelatedInformation> CreateDiagnosticRelatedInforma | |
| var rangeLength = range.EndToken.pos + range.EndToken.val.Length - range.StartToken.pos; | ||
| if (message == PostConditionFailingMessage) { | ||
| var postcondition = entryDocumentsource.Substring(range.StartToken.pos, rangeLength); | ||
| message = $"Could not prove this postcondition: {postcondition}"; | ||
| } else if (message == "Related location") { | ||
| var tokenUri = tokenForMessage.GetDocumentUri(); | ||
| if (tokenUri == entryDocumentUri) { | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,99 +1,99 @@ | ||
| AllocatedCommon.dfyi(23,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(24,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(25,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(26,30): Error: target object might not be allocated | ||
| AllocatedCommon.dfyi(27,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(28,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(29,55): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(30,53): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(31,53): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(32,59): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(33,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(34,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(35,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(37,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(46,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(47,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(48,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(49,30): Error: target object might not be allocated | ||
| AllocatedCommon.dfyi(50,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(51,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(52,55): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(53,53): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(54,53): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(55,59): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(56,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(57,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(58,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(60,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(82,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(83,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(84,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(85,30): Error: target object might not be allocated | ||
| AllocatedCommon.dfyi(86,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(87,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(88,55): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(89,53): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(90,53): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(91,59): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(92,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(93,44): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(94,35): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(95,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(96,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(97,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(98,19): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(99,19): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(100,23): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(118,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(119,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(120,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(121,30): Error: target object might not be allocated | ||
| AllocatedCommon.dfyi(122,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(123,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(124,55): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(125,53): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(126,53): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(127,59): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(128,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(129,44): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(130,35): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(131,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(132,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(133,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(134,19): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(135,19): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(136,23): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(179,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(180,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(181,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(182,31): Error: target object might not be allocated | ||
| AllocatedCommon.dfyi(183,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(184,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(185,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(186,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(187,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(188,60): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(189,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(190,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(191,44): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(192,45): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(193,41): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(194,37): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(195,57): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(196,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(197,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(198,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(199,20): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(200,9): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(201,24): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(202,27): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(218,5): Error: insufficient reads clause to read field | ||
| AllocatedCommon.dfyi(225,5): Error: insufficient reads clause to read field | ||
| AllocatedCommon.dfyi(284,9): Error: Could not prove function precondition | ||
| AllocatedCommon.dfyi(284,15): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(301,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(302,26): Error: Could not prove assertion | ||
| AllocatedCommon.dfyi(310,9): Error: Could not prove assertion | ||
|
|
||
| Dafny program verifier finished with 15 verified, 97 errors |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The convention in the rest of the messages is for them to start with a lower-case letter.