Description
Issue Info
CBMC version: 5.10
Operating system: Ubuntu 20.04.1 LTS
Exact command line resulting in the issue: cbmc stringCompare.c --function stringCompare_HARNESS --pointer-check --unwind 2 --unwinding-assertions --trace
What behaviour did you expect: No "pointer outside object bounds" error
What happened instead: Pointer outside object bounds error
Issue Description
The function should be a generic string comparer that works under the assumption that the strings are properly \0 terminated. The verification is currently set up with the assumption __CPROVER_assume(2 == size_str) just for simplification.
Two pointer out of bounds properties generated by the --pointer-check argument fail. It is caused by the dereferencing of s1 and s2 at line 13. I don't believe that it is possible for there to be an error, but I could be wrong. Changing int size_str; at line 18 to int size_str = 2; resolves the errors and gives the expected proof.
Code
int stringCompare(const char* s1, const char* s2) {
if (s1 == s2)
return 0;
while (*s1 == *s2)
{
if (*s1 == '\0')
return 0;
++s1;
++s2;
}
return *s1 - *s2; //out of bounds FAILURE (both for s1 and s2)
}
void stringCompare_HARNESS(){
int size_str; //changing this to 'int size_str = 2;' resolves the out of bounds error
__CPROVER_assume(2 == size_str);
char str1[size_str];
char str2[size_str];
__CPROVER_assume(str1[size_str-1] == '\0');
__CPROVER_assume(str2[size_str-1] == '\0');
stringCompare(str1,str2);
}
Output
...
Violated property:
file github-issue.c line 13 function stringCompare
dereference failure: pointer outside object bounds in *s1
OBJECT_SIZE(s1) >= 1ul + (unsigned long int)POINTER_OFFSET(s1) && POINTER_OFFSET(s1) >= 0l || DYNAMIC_OBJECT(s1)
Violated property:
file github-issue.c line 13 function stringCompare
dereference failure: pointer outside object bounds in *s2
OBJECT_SIZE(s2) >= 1ul + (unsigned long int)POINTER_OFFSET(s2) && POINTER_OFFSET(s2) >= 0l || DYNAMIC_OBJECT(s2)
** 2 of 29 failed (2 iterations)
VERIFICATION FAILED