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-plain x=1 y=11 *r=11 (r==p)=true


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


cerberus-concrete-PVI-ae-udi x=1 y=11 *r=11 (r==p)=true


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


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


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


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


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


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


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


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


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


clang-7.0.1-O3-no-strict-aliasing 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