search

viperproject / silver

Definition of the Viper intermediate verification language.
Mozilla Public License 2.0
78 stars 40 forks source link

Implement filtering of duplicate errors in SilFrontend #778

Closed marcoeilers closed 6 months ago

marcoeilers commented 6 months ago

The intention is to avoid reporting two errors via stdout that have the exact same message and position, which provides no value to the user. Currently, Silicon implements this itself, but Carbon does not. This PR adds an implementation in Silver to replace the one in Silicon (and in the process ensure that the filtering only happens when outputting to stdout, since the filtering can cause issues for frontends, see https://github.com/viperproject/silicon/issues/735).

fpoli commented 6 months ago

How does the backend know that the errors are going to be reported via stdout? Is the assumption that SilFrontend will only be used for command-line error reporting?

marcoeilers commented 6 months ago

SilFrontend is basically always used, but the finish method where the filtering now happens is only called from execute, which is not called when the frontend API is used.

fpoli commented 6 months ago

Thanks! Could it be worth adding a comment to finish and/or execute reminding that it should not be used by frontends because of this filtering?

fpoli commented 6 months ago

Thanks! Could it be worth adding a comment to finish and/or execute reminding that it should not be used by frontends because of this filtering?

I just realized that execute already mentions the command-line use case. It might also make sense on finish given that it's not private.