Reporting of all errors in the entity result messages#677
Merged
Conversation
… at hand) as Silicon will report at the very end
ArquintL
changed the title
mschwerhoff
approved these changes
Jan 6, 2023
mschwerhoff
left a comment
mschwerhoff
left a comment
Contributor
There was a problem hiding this comment.
I left two comments, otherwise OK.
Member
Author
|
bors merge |
marcoeilers
approved these changes
Jan 6, 2023
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
Use case for expected errors
Josua Stuck has added the concept of expected verification errors which make Silicon continue despite the occurrence of an error. This feature is in particular used by the refute plugin that marks all encoded refute statements as expected verification errors. These expected errors won't be reported to the user by the refute plugin and instead the plugin produces verification errors for encoded refute statements for which no error has been encountered by Silicon.
Keeping track of expected errors in Silicon
Silicon keeps track of these expected and encountered verification errors in the
previousfield of Silicon'sVerificationResult. It seems that the first encountered error is the verification result and all subsequent verification errors (due to continuing with verifying the input) are placed in thepreviousfield.Post-processing expected errors - so far
The
DefaultMainVerifierused to produce verification results per member while ignoring thepreviousfield, i.e. the first encountered error is returned.Siliconline 247 retrieved the errors encountered after the first one by taking thepreviousfield into account and flatting all verification results.Issue
DefaultMainVerifieris responsible for emitting entity verification result messages. Since theDefaultMainVerifierdoes not consider thepreviousfield of verification results, entity verification result messages contain different (i.e. a subset) of errors compared to Silicon's overall result (when considering the errors for the same member).This behavior is problematic in the context of Silver #641 since plugins will handle entity verification result such that the ViperServer & the IDE support plugins (see ViperServer #99).
Post-processing expected errors - new
This PR basically moves
Siliconline 247 intoDefaultMainVerifierto ensure that the union of all entity verification results (hopefully) correspond to the overall result returned by Silicon. Note however that grouping, sorting, and dealing with branch conditions have been left inSiliconas imho this concerns more errors will be printed and it's not immediately clear whether this functionality can be as easily moved intoDefaultMainVerifier, even though this could make sense in the long run.