Discuss how to report internal tool errors

[viper-admin]

Created by @mschwerhoff on 2017-09-25 10:00
Last updated on 2017-09-25 10:12

Silicon and Carbon sometimes report internal errors, e.g. because the interaction with Z3 or Boogie didn't go as expected, or because a runtime assertion was violated. Tool users should be informed about the internal error; however, there are a few things to keep in mind:

• The reported error message should, by default, be concise and not display (too many) internals, e.g. the stack trace corresponding to the failed runtime assertion or Boogie's raw output
• The error message should nevertheless hint at the underlying problem. In particular in the case of failing interaction with Z3 or Boogie, in which case an experienced user might be able to overcome the problem, e.g. because of insufficient OS permissions to access an executable file or because the installed Z3 version has a known bug and needs to be updated.
• Providing helpful information (to non-developers) in the case of an internal runtime violation is typically not possible and the corresponding error message should thus be concise and rather generic. However, it should be possible to obtain further information (such as a stack trace), e.g. by setting a configuration option of the tool or the IDE. This can again be useful for experienced users.

[viper-admin]

@mschwerhoff commented on 2017-09-25 10:12

Related issues:

• IDE: Error classification functionality could be handled in Silver / backends (and special-case unexpected/internal errors) #57
• Silicon: #306
• Carbon:
  #157,
  #178,
  #184,
  #189