We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 2cec374 commit 56c3499Copy full SHA for 56c3499
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