Allow users to only replace calls to "proved" functions with contracts

[feliperodri]

We should prevent users from using contracts for unproven functions, since this could lead to unsound results.

I don't think this could be built into CBMC because this would require a "global" view of a project -- track contracts that have been already proved and can be "trusted".
This would probably be a CI script that implements a top-sort over call graph and verifies functions bottom-up in the call tree, i.e. first "enforce" contracts for callee functions and then replace them in the caller's body if the contracts are found to be correct.

Actually, I think there may be good reasons to do this. Doing this is a case of completing a proof under some assumptions. I would prefer to do something a little more relaxed. Either

1. Allow this in general, but have CI report all functions used but not checked.
2. Allow this only for functions in some list supplied by the user so it is not done accidentally ... and still have the CI report all such functions used but not checked.