Example: pointer_offset_from_int_subtraction_global_yx.c

up: index
prev: pointer_offset_from_int_subtraction_global_xy.c
next: pointer_offset_from_int_subtraction_auto_xy.c

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

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

Experimental data (what does this mean?) 



cerberus-concrete-PVI Undefined behaviour: out of bounds pointer at memory store at 15:5-12


cerberus-concrete-PNVI Addresses: &x=92 &y=88 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


gcc-8.1-O0 Addresses: &x=6294132 &y=6294128 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


gcc-8.1-O2 Addresses: &x=6293968 &y=6293972 offset=4 
x=1 y=11 *p=11 *q=11


gcc-8.1-O3 Addresses: &x=6293968 &y=6293972 offset=4 
x=1 y=11 *p=11 *q=11


gcc-8.1-O2-no-strict-aliasing Addresses: &x=6293968 &y=6293972 offset=4 
x=1 y=11 *p=11 *q=11


gcc-8.1-O3-no-strict-aliasing Addresses: &x=6293968 &y=6293972 offset=4 
x=1 y=11 *p=11 *q=11


clang-6.0-O0 Addresses: &x=6295612 &y=6295608 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


clang-6.0-O2 Addresses: &x=6295612 &y=6295608 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


clang-6.0-O3 Addresses: &x=6295612 &y=6295608 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


clang-6.0-O2-no-strict-aliasing Addresses: &x=6295612 &y=6295608 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


clang-6.0-O3-no-strict-aliasing Addresses: &x=6295612 &y=6295608 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


clang-6.0-UBSAN Addresses: &x=6495060 &y=6495056 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


clang-6.0-ASAN Addresses: &x=7433120 &y=7433056 offset=18446744073709551552 
x=1 y=11 *p=11 *q=11


clang-6.0-MSAN Addresses: &x=7043828 &y=7043824 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


icc-19-O0 Addresses: &x=6294412 &y=6294408 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


icc-19-O2 Addresses: &x=6309572 &y=6309568 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


icc-19-O3 Addresses: &x=6309572 &y=6309568 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


icc-19-O2-no-strict-aliasing Addresses: &x=6309572 &y=6309568 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


icc-19-O3-no-strict-aliasing Addresses: &x=6309572 &y=6309568 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


compcert-3.4 Addresses: &x=6295620 &y=6295616 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


compcert-3.4-O Addresses: &x=6295620 &y=6295616 offset=18446744073709551612 
x=1 y=11 *p=11 *q=11


kcc-1.0 Addresses: &x=0 &y=0 offset=9223372036854775807 
Computing pointer difference between two different objects:
      > in main at pointer_offset_from_int_subtraction_global_yx.c:9: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

Printing an unspecified value:
      > in printf at pointer_offset_from_int_subtraction_global_yx.c:10:3
        in main at pointer_offset_from_int_subtraction_global_yx.c:10:3

    Unspecified value or behavior (USP-STDIO2):
        see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1

A pointer (or array subscript) outside the bounds of an object:
      > in main at pointer_offset_from_int_subtraction_global_yx.c:12: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

Conversion from an integer to non-null pointer:
      > in main at pointer_offset_from_int_subtraction_global_yx.c:12:3

    Implementation defined behavior (IMPL-CCV13):
        see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3
        see CERT section INT36-C http://rvdoc.org/CERT/INT36-C

Found pointer that refers outside the bounds of an object + 1:
      > in main at pointer_offset_from_int_subtraction_global_yx.c:12: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_int_subtraction_global_yx.c:14: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_int_subtraction_global_yx.c:14: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