RFC: Output - Alternative check format

[adpaco-aws]

Requested feature: Kani checks are generally reported as:

Check <index>: <property name>
     - Status: <status>
     - Description: <description>
     - Location: <location> in <function>

There are a few problems with this output:

1. <index> doesn't have a concrete purpose. These indexes are assigned while printing checks but they aren't used for anything else.
2. <property name> are just the property names used by CBMC. The general format for property names is <function>.<class>.<counter> where <function> is the function name (note: this information gets repeated in the "Location" line), <class> is one of the property classes defined in CBMC, and <counter> is another index assigned in CBMC.
3. The checks define the information they print on each check (i.e., the <status> is preceded by "Status", <description> is preceded by "Description:", etc.). This clutters the output and is unnecessary once the user is familiar with it. Definitions should come from the documentation instead.

Because of that, the requested feature is to use an alternative format that resembles the rustc output, containing not only the information being currently displayed, but also includes better diagnostics and potentially hints to resolve issues.

Use case: General Kani UI.

Link to relevant documentation (Rust reference, Nomicon, RFC): Errors and Lints in rustc development

Test case:

<code>

[jaisnan]

The change would be breaking the VS Code extension. Is there any way to ease the transition to the new output from Kani?

[adpaco-aws]

Acknowledged, although I wonder which specific parts would get broken. Structured output is probably the easiest way to avoid this.

[jaisnan]

The only parts I see breaking are the message creation parts. We parse Kani's output directly so it would break that, but nothing else. Concrete-playback and the links don't come from parsing the output so they should be fine.