Skip to content

__CPROVER_is_cstring() Ignored in CBMC Verification #8599

Open
@zhoulaifu

Description

@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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions