Create a `cover` statement to RMC

[celinval]

Requested feature: Provide a functionality to RMC to allow users to prove reachability. I.e., prove that there is at least one path where the provided statement is true.
Use case: Provides more insight to proof harnesses allowing users to ensure that their harnesses are not over-constrained.
Link to relevant documentation (Rust reference, Nomicon, RFC):
Is this a breaking change? No

Test case:

#[proof]
pub fn check_update() {
    // Write any value to the database.
    let database = rmc::nondet::<MyDatabase>();
    let key = rmc::nondet::<Key>();
    let v1 = rmc::nondet::<Value>();
    database.write(key, v1);

    // Write any other value to the database under the same key.
    let v2 = rmc::nondet::<Value>();
    database.write(key, v2);

    // Make sure v1 may be different than v2. It' OK if it's equal though.
    // Proof should fail if this is always false though.
    rmc::cover(v1 != v2);

    // Verify read gets the latest value.
    assert!(database.read(key) == v2);
}

This dummy harness shows how the harness runs under every single value combination, and that the last read is reachable under scenarios where v1 is different than v2. This is different than using an assume or another assert statement, since it won't restrict the search space.

Note that the verification should fail if the cover statement is unreachable.

[celinval]

You can enable __CPROVER_cover in cbmc:

cbmc <target> --cover cover

[celinval]

There are a couple issues with __CPROVER_cover which is being tracked here: diffblue/cbmc#6613