Example: pointer_arith_algebraic_properties_2_global.c

#include <stdio.h>
#include <inttypes.h>
int y[2], x[2];
int main() {
  int *p=(int*)(((uintptr_t)&(x[0])) + 
    (((uintptr_t)&(y[1]))-((uintptr_t)&(y[0]))));
  *p = 11;  // is this free of undefined behaviour?
  printf("x[1]=%d *p=%d\n",x[1],*p);
  return 0;
}
[link to test in Cerberus and Compiler Explorer]

Experimental data (what does this mean?) 



gcc-8.1-O0 x[1]=11 *p=11


gcc-8.1-O2 x[1]=11 *p=11


gcc-8.1-O3 x[1]=11 *p=11


gcc-8.1-O2-no-strict-aliasing x[1]=11 *p=11


gcc-8.1-O3-no-strict-aliasing x[1]=11 *p=11


clang-6.0-O0 x[1]=11 *p=11


clang-6.0-O2 x[1]=11 *p=11


clang-6.0-O3 x[1]=11 *p=11


clang-6.0-O2-no-strict-aliasing x[1]=11 *p=11


clang-6.0-O3-no-strict-aliasing x[1]=11 *p=11


clang-6.0-UBSAN x[1]=11 *p=11


clang-6.0-ASAN x[1]=11 *p=11


clang-6.0-MSAN x[1]=11 *p=11


icc-19-O0 x[1]=11 *p=11


icc-19-O2 x[1]=11 *p=11


icc-19-O3 x[1]=11 *p=11


icc-19-O2-no-strict-aliasing x[1]=11 *p=11


icc-19-O3-no-strict-aliasing x[1]=11 *p=11


cerberus-concrete BEGIN EXEC[0]
Undefined [pointer_arith_algebraic_properties_2_global.c:7:3-5]{id: [UB043_indirection_invalid_value]}
END EXEC[0]
Time spent: 0.017937 seconds


cerberus-symbolic 

gcc-4.9-shadowprov x[1]=11 *p=11


CHERI:MIPS-O0 x[1]=11 *p=11


CHERI:MIPS-O2 x[1]=11 *p=11


CHERI:MIPS-O2-no-strict-aliasing x[1]=11 *p=11


CHERI:CHERI-O0-uintcap-addr-exact-equals x[1]=11 *p=11


CHERI:CHERI-O2-uintcap-addr-exact-equals x[1]=11 *p=11


CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr-exact-equals x[1]=11 *p=11


CHERI:CHERI-O0-uintcap-offset-exact-equals x[1]=11 *p=11


CHERI:CHERI-O2-uintcap-offset-exact-equals x[1]=11 *p=11


CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset-exact-equals x[1]=11 *p=11


CHERI:CHERI-O0-uintcap-addr x[1]=11 *p=11


CHERI:CHERI-O2-uintcap-addr x[1]=11 *p=11


CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr x[1]=11 *p=11


CHERI:CHERI-O0-uintcap-offset x[1]=11 *p=11


CHERI:CHERI-O2-uintcap-offset x[1]=11 *p=11


CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset x[1]=11 *p=11


RV-Match exit codes: compile 0 / execute 1
pointer_arith_algebraic_properties_2_global.c:5:3: warning: Conversion from an integer to non-null pointer.

    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



ch2o pointer_arith_algebraic_properties_2_global.c:2:10: fatal error: inttypes.h: No such file or directory
 #include <inttypes.h>
          ^~~~~~~~~~~~
compilation terminated.


compcert-3.2 x[1]=11 *p=11


compcert-3.2-O x[1]=11 *p=11


compcert-3.2-interp Time 0: calling main()
--[step_internal_function]-->
Time 1: in function main, statement
  p = (int *) ((unsigned int) &*. + ((unsigned int) &. - (unsigned int) &.));
  *p = 11;
  printf(__stringlit_1, *(. + 1), *p);
  return 0;
  return 0;
--[step_seq]-->
Time 2: in function main, statement
  p = (int *) ((unsigned int) &*. + ((unsigned int) &. - (unsigned int) &.));
  *p = 11;
  printf(__stringlit_1, *(. + 1), *p);
  return 0;
--[step_seq]-->
Time 3: in function main, statement
  p = (int *) ((unsigned int) &*. + ((unsigned int) &. - (unsigned int) &.));
--[step_do_1]-->
Time 4: in function main, expression
  p = (int *) ((unsigned int) &*. + ((unsigned int) &. - (unsigned int) &.))
--[red_var_local]-->
Time 5: in function main, expression
  <loc p> =
    (int *) ((unsigned int) &*. + ((unsigned int) &. - (unsigned int) &.))
--[red_var_global]-->
Time 6: in function main, expression
  <loc p> =
    (int *) ((unsigned int) &*. + ((unsigned int) &. - (unsigned int) &.))
--[red_rvalof]-->
Time 7: in function main, expression
  <loc p> =
    (int *) ((unsigned int) &*. + ((unsigned int) &. - (unsigned int) &.))
--[red_binop]-->
Time 8: in function main, expression
  <loc p> =
    (int *) ((unsigned int) &*. + ((unsigned int) &. - (unsigned int) &.))
--[red_deref]-->
Time 9: in function main, expression
  <loc p> =
    (int *) ((unsigned int) &<loc x>
              + ((unsigned int) &. - (unsigned int) &.))
--[red_addrof]-->
Time 10: in function main, expression
  <loc p> =
    (int *) ((unsigned int) <ptr x>
              + ((unsigned int) &. - (unsigned int) &.))
--[red_cast]-->
Time 11: in function main, expression
  <loc p> = (int *) (<ptr x> + ((unsigned int) &. - (unsigned int) &.))
--[red_var_global]-->
Time 12: in function main, expression
  <loc p> = (int *) (<ptr x> + ((unsigned int) &. - (unsigned int) &.))
--[red_rvalof]-->
Time 13: in function main, expression
  <loc p> = (int *) (<ptr x> + ((unsigned int) &. - (unsigned int) &.))
--[red_binop]-->
Time 14: in function main, expression
  <loc p> = (int *) (<ptr x> + ((unsigned int) &. - (unsigned int) &.))
--[red_deref]-->
Time 15: in function main, expression
  <loc p> = (int *) (<ptr x> + ((unsigned int) &. - (unsigned int) &.))
--[red_addrof]-->
Time 16: in function main, expression
  <loc p> =
    (int *) (<ptr x> + ((unsigned int) <ptr y+4> - (unsigned int) &.))
--[red_cast]-->
Time 17: in function main, expression
  <loc p> = (int *) (<ptr x> + (<ptr y+4> - (unsigned int) &.))
--[red_var_global]-->
Time 18: in function main, expression
  <loc p> = (int *) (<ptr x> + (<ptr y+4> - (unsigned int) &.))
--[red_rvalof]-->
Time 19: in function main, expression
  <loc p> = (int *) (<ptr x> + (<ptr y+4> - (unsigned int) &.))
--[red_binop]-->
Time 20: in function main, expression
  <loc p> = (int *) (<ptr x> + (<ptr y+4> - (unsigned int) &.))
--[red_deref]-->
Time 21: in function main, expression
  <loc p> = (int *) (<ptr x> + (<ptr y+4> - (unsigned int) &.))
--[red_addrof]-->
Time 22: in function main, expression
  <loc p> = (int *) (<ptr x> + (<ptr y+4> - (unsigned int) <ptr y>))
--[red_cast]-->
Time 23: in function main, expression
  <loc p> = (int *) (<ptr x> + (<ptr y+4> - <ptr y>))
Stuck state: in function main, expression
  <loc p> = (int *) (<ptr x> + (<ptr y+4> - <ptr y>))
Stuck subexpression: <ptr y+4> - <ptr y>
ERROR: Undefined behavior
In file included from pointer_arith_algebraic_properties_2_global.c:1:
In file included from /usr/include/stdio.h:64:
In file included from /usr/include/_stdio.h:68:
/usr/include/sys/cdefs.h:81:2: warning: "Unsupported compiler detected" [-W#warnings]
#warning "Unsupported compiler detected"
 ^
1 warning generated.