Inconsistent behaviour with --pointer-overflow-check

[marcusgranstroem]

CBMC version: 5.15.0
Operating system: Ubuntu 20.04.2 LTS
Exact command line resulting in the issue: cbmc simple_pointer.c --pointer-overflow-check
What behaviour did you expect: VERIFICATION SUCCESSFUL
What happened instead: VERIFICATION FAILED

I am having some troubles with --pointer-overflow-check where I get reported violations when a negative index is being passed.

I use this simple program simple_pointer.c to illustrate the issue:

int
main()
{
	const char	*msg = "CBMC";
	const char	*ptr;

	ptr = msg + 1;

#ifdef BRACKET
	__CPROVER_assert(ptr[-1] == msg[0], "Bracket notation");
#elif SUBTRACT
	__CPROVER_assert(*(ptr - 1) == msg[0], "Manual pointer deref");
#else
	__CPROVER_assert(*(ptr + (-1)) == msg[0], "Manual pointer deref");
#endif

	return (0);
}

These variants should (in my opinion) yield the same result, but that is not what happens.

cbmc simple_pointer.c --pointer-overflow-check -D BRACKET

** Results:
simple_pointer.c function main
[main.overflow.1] line 7 pointer arithmetic overflow on + in msg + (signed long int)1: SUCCESS
[main.assertion.1] line 10 Bracket notation: SUCCESS
[main.overflow.2] line 10 pointer arithmetic overflow on + in ptr + (signed long int)-1: FAILURE
[main.overflow.3] line 10 pointer arithmetic overflow on + in msg + (signed long int)0: SUCCESS

** 1 of 4 failed (2 iterations)
VERIFICATION FAILED

cbmc simple_pointer.c --pointer-overflow-check -D SUBTRACT

** Results:
simple_pointer.c function main
[main.overflow.1] line 7 pointer arithmetic overflow on + in msg + (signed long int)1: SUCCESS
[main.assertion.1] line 12 Manual pointer deref: SUCCESS
[main.overflow.2] line 12 pointer arithmetic overflow on - in ptr - (signed long int)1: SUCCESS
[main.overflow.3] line 12 pointer arithmetic overflow on + in msg + (signed long int)0: SUCCESS

** 0 of 4 failed (1 iterations)
VERIFICATION SUCCESSFUL

cbmc simple_pointer.c --pointer-overflow-check

** Results:
simple_pointer.c function main
[main.overflow.1] line 7 pointer arithmetic overflow on + in msg + (signed long int)1: SUCCESS
[main.assertion.1] line 14 Manual pointer deref: SUCCESS
[main.overflow.2] line 14 pointer arithmetic overflow on + in ptr + (signed long int)-1: FAILURE
[main.overflow.3] line 14 pointer arithmetic overflow on + in msg + (signed long int)0: SUCCESS

** 1 of 4 failed (2 iterations)
VERIFICATION FAILED

Does anyone know why i get these results and is it a bug or intentional?

[tautschnig]

This has been fixed in 49481e2 (#5849), which is included in version 5.25.0 (and all later versions).