__CPROVER_is_cstring() Ignored in CBMC Verification

[zhoulaifu]

Description

I am using CBMC version 6.4.1 on macOS (ARM64) and encountered an issue where CBMC ignores __CPROVER_is_cstring().

I expected CBMC to enforce that input is a valid null-terminated string, but instead, I received the following warning:

warning: ignoring is_cstring

This seems to indicate that __CPROVER_is_cstring() is not being applied, which affects how CBMC explores symbolic string inputs.

---

Minimal Reproducible Example

Here is a simplified C program that should trigger a failure if the input starts with "HI":

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

// Function that processes input
void process_input() {
    char input[10];

    // Assume input is a valid C string
    __CPROVER_assume(__CPROVER_is_cstring(input));

    // Fail if input starts with "HI"
    if (input[0] == 'H' && input[1] == 'I') {
        assert(0);  // Force CBMC to find failing input
    }
}

// Harness function for CBMC
void harness() {
    process_input();
}

Command Used

cbmc file2.c --function harness --trace --unwind 5 --no-standard-checks

---

Unexpected Behavior

1. CBMC does not enforce __CPROVER_is_cstring()

   • I expected CBMC to ensure input is null-terminated and allow proper symbolic string generation.
   • Instead, I see this warning:

     warning: ignoring is_cstring
     

   • This suggests CBMC did not apply the assumption, leading to incorrect symbolic execution.

2. Workaround using strlen() instead of __CPROVER_is_cstring()

   • When I manually enforce:

     __CPROVER_assume(input[9] == '\0');
     __CPROVER_assume(strlen(input) < 9);

     The verification works, but I now need --unwind to avoid issues with strlen() being treated as a loop.