Inconsistent wording for verification success and failure

[reuk]

CBMC prints VERIFICATION FAILED on failure, but VERIFICATION SUCCESSFUL on success. Shouldn't it be FAILED|SUCCEEDED, UNSUCCESSFUL|SUCCESSFUL, or FAILURE|SUCCESS? As individual goals use FAILURE|SUCCESS, it seems sensible to use this scheme for the final result too.

[tautschnig]

Be warned that there is an unknown number of tools around CBMC parsing this output.

[reuk]

Maybe something for the 6.0 release then?

[tautschnig]

What's the value?

[reuk]

Improved usability. I was writing a test case for CBMC which I was expecting to succeed. I already had a test runner for a test expected to fail, which checked the output for VERIFICATION FAILED. I copied the runner, and then changed it to expect the opposite output VERIFICATION SUCCEEDED, but this didn't work. As a user, this is a bad experience, because I expect interfaces to obey the principle of least surprise. Using four different words to denote two unique states is very surprising, especially when two of those words don't form a semantic pair.

[tautschnig]

I'll leave it to others to judge the risk of breaking several companies' and existing users' tool chains over having a correct semantic pair. Making such a subtle change after ~15 years requires care.

[martin-cs]

Risk / cost : subtle and annoying breaking of wrapper scripts. In the past smaller changes to the flags / output have cause significant issues. Benefit : subjective and minimal. Many of our users do not have English as a first language so I suspect the subtly of this may be lost on them. I don't think we should make this change. There are *many* things that need this development and discussion effort *way* more urgently. For example: #896 #661

[tautschnig]

This item has been raised for #1148; I believe @martin-cs and myself have voiced opinions clearly. All others are invited to put in their weight.

[TGWDB]

Closing as there seems to be no desire to make this change and the cost/benefit does not look optimistic.