Avoid warning about not returning a value [blocks: #2548]

[tautschnig]

Compilers differ in their ability to infer dead code, and the use of INVARIANT
etc. may result in end-of-function being reachable when they are configured
as no-ops. Make compilers happy, even when that may result in statements that
really shouldn't be reachable.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• 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.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[kroening]

Won't that backfire, i.e., generate warnings about dead code?

[tautschnig]

Won't that backfire, i.e., generate warnings about dead code?

Not as far as I can tell, but maybe #2548 has other changes hiding such warnings, so we'll see when CI passes over here (where there really is just this one commit).

[allredj]

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

[peterschrammel]

That's quite awkward. Hm... We could have a variant of these macros that take the return value to make this less ugly (but maybe also more confusing).

[kroening]

I am wondering whether the goal here can be achieved by means of the right compiler annotation for "UNREACHABLE" for Visual Studio?
Or turn off the "missing return value" warning in UNREACHABLE?

[smowton]

Some use of __declspec(noreturn) on a wrapper function ought to do the trick AFAICT

[kroening]

@smowton these functions will return, just somewhere else, with a return statement. It needs to be an annotation that says "I promise we won't get here". It might be doable to do that with a throw on VS.

[smowton]

? The important thing here is if we somehow hit an UNREACHABLE then control will not return to the callsite. That should stop VS from wanting a return statement.

[kroening]

The relevant function already has a __declspec(noreturn). The problem appears to be that MSVC can't infer that

if(!(CONDITION))
   invariant_violated...(...);

doesn't have a successor for CONDITION = false.

[kroening]

@tautschnig Special-casing the UNREACHABLE macro appears to work!

[tautschnig]

@kroening I believe I have now implemented what you meant by special-casing, but please do confirm.

[allredj]

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

[tautschnig]

Marking do-not-merge: I was likely mislead, the fix might be much simpler, investigating in #2310.

[tautschnig]

@kroening @owen-jones-diffblue @smowton @kroening You might all want to take another look as I have completely reworked the commits in this PR. The proper fix was much simpler than the intermediate versions that I had, and to an extent boils down to fixing a single typo...

[allredj]

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