Goto programs with missing function bodies should not be considered well-formed

[tautschnig]

Once #1889 is merged we should be in a good position to disallow any analysis on goto programs that contain function calls to either completely undeclared functions (should never be allowed) or functions without a body. Input programs of course contain such code with varying assumptions on non-determinism, but an analysis should not make its own private assumptions about this. Instead, user-specified transformations on goto programs should be run before any analysis to produce function bodies. In any analysis, functions having non-empty bodies should be an invariant rather than a conditional check.

[esteffin]

There are 2 scenarios here:

1. undeclared functions,
2. (declared) functions without a body.

For scenario 1 we are currently issuing a warning during type-checking and one during symex (this latter warns about it being a function without a body).
For scenario 2 we just issue the warning during symex about function without body.

We understand the consideration behind scenario 1 (blocking by throwing an error when encountering undeclared functions).

Regarding scenario 2 we agree that the current assumption that functions with no body don't have side-effects on arguments and global variables is very strong.
However there are legitimate use-cases where we use functions with no body to generate nondeterministic values and these use-cases may introduce frictions when we try to pass the changes.

Are there any considerations that we are missing here for scenario 2?