Example: pointer_offset_xor_auto.c

up: index
prev: pointer_offset_xor_global.c
next: provenance_tag_bits_via_uintptr_t_1.c

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

    #include <stdio.h>
    #include <inttypes.h>
    int main() {
      int x=1, y=2;
      int *p = &x;
      int *q = &y;
      uintptr_t i = (uintptr_t) p;
      uintptr_t j = (uintptr_t) q;
      uintptr_t k = i ^ j;
      uintptr_t l = k ^ i;
      int *r = (int *)l;
      // are r and q now equivalent?  
      *r = 11;     // does this have defined behaviour?             
      _Bool b = (r==q); 
      printf("x=%i y=%i *r=%i (r==p)=%s\n",x,y,*r,
             b?"true":"false");  
    }
[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 13:3-10


cerberus-concrete-PNVI x=1 y=11 *r=11 (r==p)=true


gcc-8.1-O0 x=1 y=11 *r=11 (r==p)=true


gcc-8.1-O2 x=1 y=11 *r=11 (r==p)=true


gcc-8.1-O3 x=1 y=11 *r=11 (r==p)=true


gcc-8.1-O2-no-strict-aliasing x=1 y=11 *r=11 (r==p)=true


gcc-8.1-O3-no-strict-aliasing x=1 y=11 *r=11 (r==p)=true


clang-6.0-O0 x=1 y=11 *r=11 (r==p)=true


clang-6.0-O2 x=1 y=11 *r=11 (r==p)=true


clang-6.0-O3 x=1 y=11 *r=11 (r==p)=true


clang-6.0-O2-no-strict-aliasing x=1 y=11 *r=11 (r==p)=true


clang-6.0-O3-no-strict-aliasing x=1 y=11 *r=11 (r==p)=true


clang-6.0-UBSAN x=1 y=11 *r=11 (r==p)=true


clang-6.0-ASAN x=1 y=11 *r=11 (r==p)=true


clang-6.0-MSAN x=1 y=11 *r=11 (r==p)=true


icc-19-O0 x=1 y=11 *r=11 (r==p)=true


icc-19-O2 x=1 y=11 *r=11 (r==p)=true


icc-19-O3 x=1 y=11 *r=11 (r==p)=true


icc-19-O2-no-strict-aliasing x=1 y=11 *r=11 (r==p)=true


icc-19-O3-no-strict-aliasing x=1 y=11 *r=11 (r==p)=true


compcert-3.4 x=1 y=11 *r=11 (r==p)=true


compcert-3.4-O x=1 y=11 *r=11 (r==p)=true


kcc-1.0 exit codes: compile 0 / execute 139
Conversion from an integer to non-null pointer:
      > in main at pointer_offset_xor_auto.c:11: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

Indeterminate value used in an expression:
      > in main at pointer_offset_xor_auto.c:11:3

    Undefined behavior (UB-CEE2):
        see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4
        see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9
        see C11 section 6.8 http://rvdoc.org/C11/6.8
        see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2
        see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-C
        see MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Dereferencing a null pointer:
      > in main at pointer_offset_xor_auto.c:13:3

    Undefined behavior (UB-CER3):
        see C11 section 6.5.3.2:4 http://rvdoc.org/C11/6.5.3.2
        see C11 section J.2:1 item 43 http://rvdoc.org/C11/J.2
        see CERT-C section EXP34-C http://rvdoc.org/CERT-C/EXP34-C
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Execution failed (configuration dumped)