CBMC: Unify listings of used functions

[hanno-becker]

This commit unifies the listing of functions called by contract to the format

USED_FUNCTIONS = foo
USED_FUNCTIONS += bar0
USED_FUNCTIONS += bar1
...
USE_FUNCTION_CONTRACTS=$(addprefix $(NAMESPACE_PREFIX),$(USED_FUNCTIONS))

This makes it easier to

• see what is being used,
• add/remove functions
• change the namespace prefix

[mkannwischer]

Thanks for cleaning this up - I appreciate switching everything to USED_FUNCTIONS +=.
However, I think the indirect addition of mlk_ is unnecessary. I'd like to be able to copy&past function names. Do you mind removing that again?

[hanno-becker]

@mkannwischer

I'd like to be able to copy&past function names...

This is only possible because mlk is the namespace prefix in the CBMC config file. Which can be convenient, but isn't always: For example, if the function names before/after preprocessing are the same, you have no way to force the one after preprocessing. I noticed this in #1467 where I wanted to call the functions post-preprocessing (which do not have a context parameter), but couldn't, because their C name was overlayed by a macro of the same name, for which the context parameter was mandatory.

Note that the convenience you seek could be retained by using mlk_ in USED_FUNCTIONS, but stripping that when moving to USE_FUNCTION_CONTRACTs; so, USED_FUNCTIONS would be in terms of the source names, and USE_FUNCTION_CONTRACTS would be (and must be) in terms of the symbols.

[hanno-becker]

I marked this as Draft while experimenting how close this PR actually brings us to being able to change the symbol namespace.