CBMC should have a assert-false-undefined-functions option

[danielsn]

Currently, CBMC by default has a nondet return value for undefined functions, which is unsound if they have side-effects.
goto-instrument offers more fine grained control, but is difficult to use correctly, and requires customers to use a goto-instrument flow #6393
CBMC offers --havoc-undefined-functions which is better, but still not ideal. It does not support any of the other options goto-instrument has for undefined functions.

Proposal: CBMC should allow users to control what happens with undefined functions.
Minimal solution: support assert(false).

--havoc-undefined-functions
                              for any function that has no body, assign non-deterministic values to
                              any parameters passed as non-const pointers and the return value

[thomasspriggs]

I think it would be useful to make goto-instrument's --generate-function-body argument available as an argument to CBMC. That way it will be more straight forward to make sure this pass is carried out after linking is complete. I can take a look at implementing this, assuming no one else has any objections.

[kroening]

I object strongly. Every option that goto-instrument has is useful to somebody. We want to reduce the number of CBMC options, not increase them.

[thomasspriggs]

I object strongly. Every option that goto-instrument has is useful to somebody. We want to reduce the number of CBMC options, not increase them.

In which case I am happy with the idea of closing out this ticket as "won't do". Is this intended architectural direction documented anywhere? It seems like the sort of thing which would be nice to have in - doc/ADR/README.md

As an aside - Do we expect more or less all users eventually to be using goto-instrument as part of their work flow?

[thomasspriggs]

@danielsn Are you ok with us closing out this issue, or do you want to make more arguments in favour of this feature?

[thomasspriggs]

Ok. I am going to close this out, due to lack of further arguments in favour.