Add support verification of unbounded structures and loops

[danielsn]

The CBMC backend RMC uses currently only supports bounded verification. This means bugs may be missed if the are only triggered by inputs larger than the specified bounds.

Likelihood:

In practice, we found few issues (other than integer overflows) where this was a major concern in C code, and expect the same to hold for Rust.

Mitigation:

• using --unwinding-assertions to ensure that all loops are fully unwound
• Checking coverage
• Manual audit of proof harness bounds

Path to soundness:

Support function contracts and loop invariants

Documentation:

[adpaco-aws]

Marking first mitigation item as "done" since we are now using --unwinding-assertions by default (#263)

[chinmaydd]

To ensure complete support of unbounded structures, RMC might be blocked by Issue #6261 on CBMC. CBMC currently does not handle __CPROVER_constant_infinity_uint correctly.

[feliperodri]

Outdated issue. There are a number of issues tracking support for function and loop contracts as well as coverage.