String equality check enters an infinite loop

[bdalrhm]

I tried this code:

fn main() {
    let x: &str = "hello";
    assert!(x == "hello");
}

using the following command line invocation:

rmc <filename>.rs

with RMC version:

• Branch: main-152-2021-05-18
• Hash: 662d19b

I expected to see this happen: RMC verifies the assertion, terminates, and prints VERIFICATION SUCCESSFUL.

Instead, this happened: RMC goes into an infinite loop, unwinding the string comparison loop:

Unwinding loop memcmp.0 iteration 731 file <builtin-library-memcmp> line 25 function memcmp thread 0

Notice that this problem does not occur with CBMC when given the following equivalent C program:

#include <assert.h>
#include <string.h>

void main()
{
    char *x = "hello";
    assert(strcmp(x, "hello") == 0);
}

[danielsn]

This is a design issue with CBMC - if it can't constant propegate the length, it will spin forever. We can raise this as an issue with them; until then, lets just set an explicit unwinding bound.