Example: pointer_offset_from_ptr_subtraction_global_yx.c

up: index
prev: pointer_offset_from_ptr_subtraction_global_xy.c
next: pointer_offset_from_ptr_subtraction_auto_xy.c

1
2
3
4
5
6
7
8
9
10
11
12
13
14

    #include <stdio.h>
    #include <string.h> 
    #include <stddef.h>
    int y=2, x=1;
    int main() {
      int *p = &x;
      int *q = &y;
      ptrdiff_t offset = q - p;
      int *r = p + offset;
      if (memcmp(&r, &q, sizeof(r)) == 0) {
        *r = 11; // is this free of UB?
        printf("y=%d *q=%d *r=%d\n",y,*q,*r); 
      }
    }
[link to run test in Cerberus]

Experimental data (what does this mean?) 



cerberus-concrete-PVI Undefined behaviour: the subtraction of two pointers must be between pointers that points into, or just beyond, the same array object at other_location(Concrete)


cerberus-concrete-PNVI Undefined behaviour: the subtraction of two pointers must be between pointers that points into, or just beyond, the same array object at other_location(Concrete)


gcc-8.1-O0 y=11 *q=11 *r=11


gcc-8.1-O2 y=11 *q=11 *r=11


gcc-8.1-O3 y=11 *q=11 *r=11


gcc-8.1-O2-no-strict-aliasing y=11 *q=11 *r=11


gcc-8.1-O3-no-strict-aliasing y=11 *q=11 *r=11


clang-6.0-O0 y=11 *q=11 *r=11


clang-6.0-O2 y=11 *q=11 *r=11


clang-6.0-O3 y=11 *q=11 *r=11


clang-6.0-O2-no-strict-aliasing y=11 *q=11 *r=11


clang-6.0-O3-no-strict-aliasing y=11 *q=11 *r=11


clang-6.0-UBSAN y=11 *q=11 *r=11


clang-6.0-ASAN y=11 *q=11 *r=11


clang-6.0-MSAN y=11 *q=11 *r=11


icc-19-O0 y=11 *q=11 *r=11


icc-19-O2 y=11 *q=11 *r=11


icc-19-O3 y=11 *q=11 *r=11


icc-19-O2-no-strict-aliasing y=11 *q=11 *r=11


icc-19-O3-no-strict-aliasing y=11 *q=11 *r=11


compcert-3.4 y=11 *q=11 *r=11


compcert-3.4-O y=11 *q=11 *r=11


kcc-1.0 Computing pointer difference between two different objects:
      > in main at pointer_offset_from_ptr_subtraction_global_yx.c:8:3

    Undefined behavior (UB-CEA5):
        see C11 section 6.5.6:9 http://rvdoc.org/C11/6.5.6
        see C11 section J.2:1 item 48 http://rvdoc.org/C11/J.2
        see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C
        see MISRA-C section 8.18:2 http://rvdoc.org/MISRA-C/8.18
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

A pointer (or array subscript) outside the bounds of an object:
      > in main at pointer_offset_from_ptr_subtraction_global_yx.c:9:3

    Undefined behavior (UB-CEA1):
        see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6
        see C11 section J.2:1 item 46 http://rvdoc.org/C11/J.2
        see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C
        see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C
        see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C
        see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Found pointer that refers outside the bounds of an object + 1:
      > in main at pointer_offset_from_ptr_subtraction_global_yx.c:9:3

    Undefined behavior (UB-CEE3):
        see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1
        see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2
        see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C
        see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C
        see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Cannot compare pointers with different base objects using '<':
      > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19
        in main at pointer_offset_from_ptr_subtraction_global_yx.c:10:3

    Undefined behavior (UB-CERL1):
        see C11 section 6.5.8:5 http://rvdoc.org/C11/6.5.8
        see C11 section J.2:1 item 53 http://rvdoc.org/C11/J.2
        see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C
        see MISRA-C section 8.18:3 http://rvdoc.org/MISRA-C/8.18
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Comparison of unspecified value:
      > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19
        in main at pointer_offset_from_ptr_subtraction_global_yx.c:10:3

    Unspecified value or behavior (USP-CERL7):
        see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1