Warn the user if contracts are unused

[JustusAdam]

The contracts as added by #2655 ignore unused contracts. However a scenario is conceivable where a user specifies a contract for a function and expect this to be checked/enforced automatically as is the case in many other verifiers.

@feliperodri suggested we should warn the user if an "unused" contract is encountered.. This issue should serve as a discussion board for when such a warning should be issued.

Some initial questions:

• Should issuing the warning depend on reachability of the contracted code?
• What it --harness is passed?
• Should we only warn that a check is missing or also that replacement could be used?
• Should the warning depend on whether -Zfunction-contracts is enabled?