Warn the user if contracts are unused #2741
Description
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
--harnessis passed? - Should we only warn that a check is missing or also that replacement could be used?
- Should the warning depend on whether
-Zfunction-contractsis enabled?