We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 6b5c1b5 commit a89bacaCopy full SHA for a89baca
regression/cbmc-shadow-memory/strdup1/main.c
@@ -8,6 +8,9 @@ int main()
8
__CPROVER_field_decl_global("field1", (unsigned __CPROVER_bitvector[2])0);
9
10
char *s = (char *)malloc(3 * sizeof(char));
11
+ // Terminate string so that `strdup` will not call `strlen`
12
+ // on a string without a null-terminator.
13
+ s[2] = '\0';
14
assert(__CPROVER_get_field(&s[0], "field1") == 0);
15
assert(__CPROVER_get_field(&s[1], "field1") == 0);
16
0 commit comments