Add first pass of proof obligation description expressions #5317
Conversation
There was a problem hiding this comment.
There are enough of these now that it might be worth adding a flag to show the asserted expression for every proof failure. We could leave it as a hidden option until we've filled out all the options, but that would allow us to have tests for each proof obligation type as we go along.
| @@ -46,6 +46,7 @@ public static class ErrorReporterExtensions { | |||
| private const string RelatedLocationCategory = "Related location"; | |||
| public const string RelatedLocationMessage = RelatedLocationCategory; | |||
| private const string RelatedMessageCategory = "Related message"; | |||
| public const string AssertedExprCategory = "Asserted expression"; | |||
There was a problem hiding this comment.
I love that this fits in nicely with the existing reporter infrastructure!
There was a problem hiding this comment.
Indeed - for a while I thought I might need to make changes in Boogie itself in order to propagate the necessary expressions, but this worked out nicely.
| @@ -380,6 +380,8 @@ public enum IncludesModes { | |||
| [CanBeNull] private TestGenerationOptions testGenOptions = null; | |||
| public bool ExtractCounterexample = false; | |||
|
|
|||
| public bool ShowProofObligationExpressions = false; | |||
There was a problem hiding this comment.
Please don't add any fields to DafnyOptions, nor use DafnyOptions.RegisterLegacyBinding. The right way is to use DafnyOptions.RegisterLegacyUI.
Could you fix this is your next related PR?
| @@ -11,7 +11,7 @@ public static class ErrorReporterExtensions { | |||
| var usingSnippets = reporter.Options.Get(Snippets.ShowSnippets); | |||
| var relatedInformation = new List<DafnyRelatedInformation>(); | |||
| foreach (var auxiliaryInformation in error.Aux) { | |||
| if (auxiliaryInformation.Category == RelatedMessageCategory) { | |||
| if (auxiliaryInformation.Category == RelatedMessageCategory || auxiliaryInformation.Category == AssertedExprCategory) { | |||
There was a problem hiding this comment.
I'd rather not add code to a generic location such as ReporterExtensions to support a specific use-case (this PR). Did you consider using the existing RelatedMessageCategory ?
Description
Adds a first pass of proof obligation description expressions, towards resolving #2987. It also adds a new hidden option,
--show-proof-obligation-expressions, which adds to each (supported) failed proof obligation error message an equivalent Dafny assertion. This option is used to automate test for the newly added proof obligation description expressions, but this PR does not backfill tests for existing PODesc expressions.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.