Improve error message when functional method is inherited

[thk123]

This error can be erroneously triggered both when there are default methods on the interface (meaning >1 methods) or when the method is actually defined in an inherited interface (meaning 0 methods). Extend the warning message to explain both cases.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• [n.a] Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• [n/a] My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[smowton]

Oooh, hadn't thought of that

[smowton]

Consider adding a FUTURE test for this?

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 5466c08).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122986140

[smowton]

True. My shortcomings probably shouldn't serve as excuse though ;)

[thk123]

Not only is there such a test, but there is also a test for exactly this - both in lambda-unhandled-types

[thk123]

Tested here: https://github.com/diffblue/cbmc/blob/develop/jbmc/regression/jbmc/lambda-unhandled-types/test.desc#L8

(by you!! 😛 )

[smowton]

Note that test specifically looks for a stub superinterface, is that the case here?