Extend /testContracts to be able to test contracts on any function/method

[atomb]

Summary

It could be useful to allow any (compilable) contract clause to be checked at runtime. This would make it possible to test code that's difficult to prove. In the extreme case, you could compile with this turned on and /noVerify and have a system more like Eiffel.

Background and Motivation

PR #2712 introduced the /testContracts flag, which adds runtime checks for certain functions and methods. In particular it supports checking contracts dynamically on either:

• All externs
• Any extern called directly from a test

The original goal was to extend this to support a larger range of code, and not leave it restricted to externs.

Proposed Feature

Add a parameter to /testContracts, perhaps /testContracts:All to insert runtime checks for all compilable contract clauses (with warnings for any that aren't compilable, as are already present for externs).

Alternatives

No response

[atomb]

After experimenting with a command-line option that disables all filtering, therefore applying runtime contract testing to all functions and methods, there seem to be a handful of failures that show up:

• The current code fails on constructors, as it's not possible to create a new constructor that wraps an old one. We'll either need to explicitly skip constructors (and warn if they have contracts?) or come up with a cleverer encoding to deal with them.
• There's an assertion in the QuantifierExpr class that occasionally fails.
• The UselessOldLinter sometimes fails.
• Some generated wrappers fail to type check because of what I think is an instance of Dafny fails to check type characteristics in specification clauses #3150. If I'm right about that, it's a bug in the Dafny input code, not in the /testContracts implementation. Can be replicated with this file.
• Duplicate wrappers with the same name sometimes show up. Can be replicated with this file.
• Null dereference in Dafny.Resolver.FrameArrowToObjectSet. Can be replicated with this file.
• Null dereference in Triggers.TriggersCollector.TranslateToFunctionCall. Can be replicated with this file.