Error Reporting in Silver Verifiers

There are a number of features in Silver that, when verified, can cause a verification error, such as dereferencing an expression (if that expression is null), exhale statements or assertions.

A Silver verifier takes a Silver program (represented as a Silver AST) as input, and produces a potentially empty list of verification errors. If the list is empty, then the program successfully verified. Otherwise, every verification error describes one (potential) problem in the Silver program and consists of:

• A unique short string identifier for the type of error, e.g., dereference.of.null. The identifiers should be short, descriptive and all-lowercase words separated by fullstops.
• A reference to the offending Silver expression/statement.
• A severity (ERROR, WARNING, or INFO).
• Any other additional information that might be useful (might depend on the error).

Note that a Silver verifier does not output any error messages, but only returns this list. The front-end will construct user-readable error messages and output them.

Error Reporting for Translators

Typically, a program in a source language will be translated to Silver, then verified by a Silver verifier and the errors finally reported to the user. Since the Silver verifiers don't know about the source language, it is not possible for them to generate the final error message shown to the user. Rather, the translator will map every Silver verification error to a source language verification error (with its own unique identifier), and can then generate a user-friendly error message if necessary. It is still useful to have unique identifiers for these source language errors for, e.g., testing purposes (see testing).

In most cases, it is convenient to attach the source language verification errors to proof obligations in the Silver program (e.g. to an assertion) to make the mapping trivial.