Use of `--replace-call-with-contract` with function that does not have a contract should be errored

[tautschnig]

This is a soundness risk as we assume a trivial contract (with a warning, but no hard error). We should make this a hard error for it is easy enough to manually create a trivial contract when needed.

[kroening]

Sounds sensible.

[hanno-becker]

This would be very useful, yes. Otherwise it's too easy to introduce a soundness gap in the application if you have a typo in your CBMC Makefile. This happened to us in mlkem-native, luckily in a fairly benign case, but enough to be a cautionary tale.

[hanno-becker]

@tautschnig From the looks of it, this should be simple -- is it? When do you expect to have time for a fix?