RFC : turn the interpreter into the reference semantics for GOTO programs

[martin-cs]

Originally a valid GOTO program was one generated by goto_convert from the C front-end. This is not an ideal definition but it did the job for a while. As other language front-ends rise in importance it becomes a less useful definition. As a result there have been a number of questions about what constitute valid GOTO programs ( #7471 #6495 ) and their semantics ( #8258 #8223 #8196 #7072 #4323 #2031 ).

Having a declarative semantics would be mathematically and conceptually appealing but many of the practical benefits would be achieved by having an executable semantics. So, I propose turning the interpreter https://github.com/diffblue/cbmc/blob/develop/src/goto-programs/interpreter_class.h into the "formal semantics" of GOTO programs. This is mostly just documentation, adding checks, invariants and assumptions and possibly some testing.

[martin-cs]

CC @tautschnig w.r.t. our earlier discussion

[peterschrammel]

It might be worth using our test suites to automatically sanity cross-check the various implementations we have (interpretation, BMC, goto-analyzer). It's likely that they disagree in a few cases and we need to make a call which of them is actually right/intended/desired.