Confusing results with --pointer-overflow-check

[TimotheeDurand]

CBMC version: release 5.12
Operating system: x86_64-linux (Ubuntu 18.04.4)
Exact command line resulting in the issue: cbmc test.c --pointer-overflow-check
What behaviour did you expect: VERIFICATION FAILED
What happened instead: VERIFICATION SUCCESSFUL

test.c:

1  #include <stdlib.h>
2  
3
4  int main()
5  {
6      int *p = malloc(sizeof(int)*5);
7      int *p2 = p + 10;    // undefined behavior for indexing out of bounds
8      int *p3 = p - 10;    // undefined behavior for indexing out of bounds
9  
10     int arr[5];
11     int *p4 = arr + 10;  // undefined behavior for indexing out of bounds
12     int *p5 = arr - 10;  // undefined behavior for indexing out of bounds
13     return 0;
14 }                                                                                                                                                           

Greetings,

I am confused that CBMC reports no errors on the code above: The C standard specifies that incrementing a pointer to an array
further away than the sizeof(array)+1 is undefined behavior [1].
The value of the pointer p returned by malloc could very well be MAX_POINTER_ADDRESS - 7 * sizeof(int), so adding 10 to that value should trigger a pointer overflow error.

Am I making a mistake here, or is the tool not doing what I am expecting?

---

** Results:
test.c function main                                                
[main.overflow.1] line 7 pointer arithmetic overflow on + in p + (signed long int)10: SUCCESS                                           
[main.overflow.2] line 8 pointer arithmetic overflow on - in p - (signed long int)10: SUCCESS                                                                                                    
[main.overflow.3] line 11 pointer arithmetic overflow on + in arr + (signed long int)10: SUCCESS
[main.overflow.4] line 12 pointer arithmetic overflow on - in arr - (signed long int)10: SUCCESS
** 0 of 4 failed (1 iterations)                                     
VERIFICATION SUCCESSFUL             

---

[1] ISO/IEC 9899:1999 - Programming languages — C - ISO - §6.5.6 Additive operators [expr.add] para. 8, accessed 19.07.2020 at http://www.dii.uchile.cl/~daespino/files/Iso_C_1999_definition.pdf

Exact citation:

When an expression that has integer type is added to or subtracted from a pointer, the result has the type of the pointer operand. If the pointer operand points to an element of an array object, and the array is large enough, the result points to an element offset from the original element such that the difference of the subscripts of the resulting and original array elements equals the integer expression. In other words, if the expression P points to the i-th element of an array object, the expressions (P)+N (equivalently, N+(P)) and (P)-N (where N has the value n) point to, respectively, the i+n-th and i−n-th elements of
the array object, provided they exist. Moreover, if the expression P points to the last element of an array object, the expression (P)+1 points one past the last element of the array object, and if the expression Q points one past the last element of an array object, the expression (Q)-1 points to the last element of the array object. If both the pointer operand and the result point to elements of the same array object, or one past the last element of the array object, the evaluation shall not produce an overflow; otherwise, the behavior is undefined. If the result points one past the last element of the array object, it shall not be used as the operand of a unary * operator that is evaluated.

Edit: changed citation to C99 standard

[danpoe]

Thanks for reporting this. At the moment cbmc only reports an overflow when the result of pointer arithmetic cannot be represented with the pointer bit width (e.g., assuming 32-bit pointers, when adding 0xFFFFFFFF to a pointer of value 0xFF000000). There are plans however to change the semantics of --pointer-overflow-check to detect the cases you mentioned above (see discussion here: #5401 (comment))

[TimotheeDurand]

Oh, I did not know that there was an open discussion about that topic.
Thank you for the explanation.