Error classification functionality could be handled in Silver / backends (and special-case unexpected/internal errors)

[viper-admin]

Created by @alexanderjsummers on 2016-10-21 14:41
Last updated on 2017-03-05 13:43

In order to manage changes to/variants of the error message types generated by the backends, we could make the classification of errors into the kinds that the IDE cares about (apparently four types) explicit in the case classes for the errors. This would allow for specialising/changing errors in the future without changing the IDE logic.

One extra point to generalise would be to add some kind of auxiliary information to unexpected error cases (such as Boogie producing unexpected text), so that we can specify both a "friendly" error message (to be displayed by default in the IDE error summary) and a detailed string including the command-line output, to be displayed only in the Viper output panel.

[viper-admin]

Bitbucket user rukaelin commented on 2016-10-31 08:33

silicon already outputs error tags, classifying the error. When carbon supports the JSON output format we can add it there, too.

[viper-admin]

@alexanderjsummers commented on 2016-10-31 08:45

Hi Ruben,

Does Silicon specify only the same tags that the testing infrastructure depends on, or does it also specify (in the JSON) whether the IDE should treat the error as an internal one, etc.? It is this logic that I meant to describe - where is the classification of an error made in terms of how it should be handled by the IDE?

[viper-admin]

@aterga commented on 2016-10-31 08:51

Just to clarify a bit, we discussed this question in detail with Alex. Seem like there are cases in which we have a concrete error tag, but the way we want to represent the error in the IDE is different. We concluded that, in the general case, error tags are independent of the way we want to report the error (for example, when Carbon reports an Error encountered on the level of Boogie, I can show you this scenario some time later).

This is why we thought that the decision on how to visualize the error should be made on the level of the back-end, and not on the level of the IDE extension.

[viper-admin]

@aterga on 2017-03-05 13:43:

• changed component from (none) to Viper Protocol (Backend)