Open
Description
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
-
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.
- I expected CBMC to ensure
-
Workaround using
strlen()
instead of__CPROVER_is_cstring()
- When I manually enforce:
The verification works, but I now need
__CPROVER_assume(input[9] == '\0'); __CPROVER_assume(strlen(input) < 9);
--unwind
to avoid issues withstrlen()
being treated as a loop.
- When I manually enforce:
Metadata
Metadata
Assignees
Labels
No labels