index out of bounds exceptions don't assume(false)

[tedinski]

This is apparent in the docs/src/tutorials/loops-unwinding example. Where we get both a bounds and a pointer failure:

SUMMARY: 
 ** 2 of 350 failed
Failed Checks: index out of bounds: the length is less than or equal to the given index
 File: "./src/bounds_check.rs", line 11, in bounds_check::get_wrapped
Failed Checks: dereference failure: pointer outside object bounds
 File: "./src/bounds_check.rs", line 11, in bounds_check::get_wrapped

VERIFICATION:- FAILED

gen-c shows:

/* [KANI_REACHABILITY_CHECK] KANI_CHECK_ID_loops_unwinding.6ff84bc3::loops_unwinding_0 */
    assert(!1);
    if(var_18 == 0)
    {
      /* [KANI_CHECK_ID_loops_unwinding.6ff84bc3::loops_unwinding_0] index out of bounds: the length is less than or equal to the given index */
      assert(0);
      goto bb8;
    /* unreachable code */
    }


  bb8:
    ;

in contrast a typical assert shows:

      assert(0);
      __CPROVER_assume(0);

The result is confusing, since it seems to imply the bounds check isn't good enough and could still causing memory unsafety.

[tedinski]

This is probably a concrete example of #1056 needing to be done.