Mode for only verifying the absence of UB

[Lysxia]

There are different verification goals one may have, which result in different contracts. These are different "modes" we may want to support:

• Creusot's currently intended goal is to prevent most panics. For example, we allow the size overflow panic in Vec::push, because that's a PITA to deal with for little gain, but we forbid the out-of-bounds panic in index.
• Another choice is to only prevent UB, but with guarantees applicable even for unverified clients. In that case all public safe functions must have a true precondition, including panic! which is considered safe in this setting. Only unsafe and private functions may have preconditions other than true.
• Going in the opposite direction, it's natural to imagine another mode where all panics are forbidden, even in Vec::push, which would have to have yet another contract.
• Generalizing further, we might as well leave it entirely up to the user to decide what behaviors to forbid, defining their own modes.

In terms of implementation, I currently think that "modes" would mainly be a way to choose between different contracts. For the "no UB" mode Creusot could additionally check that public functions have no preconditions. I wonder whether this should somehow interact with #[terminating] and #[pure] attributes, or other features.

We can start with two modes to keep it simple: on top of the current "best effort" mode, I really want to add a "no UB, panics allowed" mode for the verify-rust-std challenge.

[xldenis]

Do you envision modes forming a hierarchy?