Example: pointer_arith_algebraic_properties_2_auto.c

#include <stdio.h>
#include <inttypes.h>
int main() {
int y[2], x[2];
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_auto.c:7:3-5]{id: [UB043_indirection_invalid_value]}
END EXEC[0]
Time spent: 0.017931 seconds
cerberus-symbolic BEGIN EXEC[0]
Undefined [unknown location]{id: [UB019_lvalue_not_an_object]}
END EXEC[0]
BEGIN EXEC[1]
Killed {msg: Memory WIP: TODO: load from device memory ==> PV(Prov_device, PVfromint(IVop(rem_f, IVop(+, IVfromptr(signed int, uintptr_t, PVbase(4, {main.x}), [SPE_array(signed int,IVconcrete(0))]), IVop(rem_f, IVop(-, IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(1))]), IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(0))])), IVconcrete(18446744073709551616))), IVconcrete(18446744073709551616))), [])}
END EXEC[1]
BEGIN EXEC[2]
Killed {msg: Memory WIP: tried to cast to a pointer type an (non device) integer value non-equal to zero}
END EXEC[2]
BEGIN EXEC[3]
Killed {msg: Memory WIP: TODO: load from device memory ==> PV(Prov_device, PVfromint(IVop(-, IVop(rem_f, IVop(+, IVfromptr(signed int, uintptr_t, PVbase(4, {main.x}), [SPE_array(signed int,IVconcrete(0))]), IVop(rem_f, IVop(-, IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(1))]), IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(0))])), IVconcrete(18446744073709551616))), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616))), [])}
END EXEC[3]
BEGIN EXEC[4]
Killed {msg: Memory WIP: tried to cast to a pointer type an (non device) integer value non-equal to zero}
END EXEC[4]
BEGIN EXEC[5]
Undefined [unknown location]{id: [UB019_lvalue_not_an_object]}
END EXEC[5]
BEGIN EXEC[6]
Killed {msg: Memory WIP: TODO: load from device memory ==> PV(Prov_device, PVfromint(IVop(rem_f, IVop(+, IVfromptr(signed int, uintptr_t, PVbase(4, {main.x}), [SPE_array(signed int,IVconcrete(0))]), IVop(rem_f, IVop(rem_f, IVop(-, IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(1))]), IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(0))])), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616))), IVconcrete(18446744073709551616))), [])}
END EXEC[6]
BEGIN EXEC[7]
Killed {msg: Memory WIP: tried to cast to a pointer type an (non device) integer value non-equal to zero}
END EXEC[7]
BEGIN EXEC[8]
Killed {msg: Memory WIP: TODO: load from device memory ==> PV(Prov_device, PVfromint(IVop(-, IVop(rem_f, IVop(+, IVfromptr(signed int, uintptr_t, PVbase(4, {main.x}), [SPE_array(signed int,IVconcrete(0))]), IVop(rem_f, IVop(rem_f, IVop(-, IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(1))]), IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(0))])), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616))), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616))), [])}
END EXEC[8]
BEGIN EXEC[9]
Killed {msg: Memory WIP: tried to cast to a pointer type an (non device) integer value non-equal to zero}
END EXEC[9]
BEGIN EXEC[10]
Undefined [unknown location]{id: [UB019_lvalue_not_an_object]}
END EXEC[10]
BEGIN EXEC[11]
Killed {msg: Memory WIP: TODO: load from device memory ==> PV(Prov_device, PVfromint(IVop(rem_f, IVop(+, IVfromptr(signed int, uintptr_t, PVbase(4, {main.x}), [SPE_array(signed int,IVconcrete(0))]), IVop(-, IVop(rem_f, IVop(-, IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(1))]), IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(0))])), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616))), IVconcrete(18446744073709551616))), [])}
END EXEC[11]
BEGIN EXEC[12]
Killed {msg: Memory WIP: tried to cast to a pointer type an (non device) integer value non-equal to zero}
END EXEC[12]
BEGIN EXEC[13]
Killed {msg: Memory WIP: TODO: load from device memory ==> PV(Prov_device, PVfromint(IVop(-, IVop(rem_f, IVop(+, IVfromptr(signed int, uintptr_t, PVbase(4, {main.x}), [SPE_array(signed int,IVconcrete(0))]), IVop(-, IVop(rem_f, IVop(-, IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(1))]), IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(0))])), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616))), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616))), [])}
END EXEC[13]
BEGIN EXEC[14]
Killed {msg: Memory WIP: tried to cast to a pointer type an (non device) integer value non-equal to zero}
END EXEC[14]
BEGIN EXEC[15]
Killed {msg: Memory WIP: TODO: load from device memory ==> PV(Prov_device, PVfromint(IVop(-, IVop(rem_f, IVop(+, IVfromptr(signed int, uintptr_t, PVbase(4, {main.x}), [SPE_array(signed int,IVconcrete(0))]), IVop(-, IVop(rem_f, IVop(-, IVop(rem_f, IVop(-, IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(1))]), IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(0))])), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616))), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616))), [])}
END EXEC[15]
BEGIN EXEC[16]
Killed {msg: Memory WIP: tried to cast to a pointer type an (non device) integer value non-equal to zero}
END EXEC[16]
BEGIN EXEC[17]
Undefined [unknown location]{id: [UB019_lvalue_not_an_object]}
END EXEC[17]
BEGIN EXEC[18]
Killed {msg: Memory WIP: TODO: load from device memory ==> PV(Prov_device, PVfromint(IVop(rem_f, IVop(+, IVfromptr(signed int, uintptr_t, PVbase(4, {main.x}), [SPE_array(signed int,IVconcrete(0))]), IVop(-, IVop(rem_f, IVop(-, IVop(rem_f, IVop(-, IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(1))]), IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(0))])), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616))), IVconcrete(18446744073709551616))), [])}
END EXEC[18]
BEGIN EXEC[19]
Killed {msg: Memory WIP: tried to cast to a pointer type an (non device) integer value non-equal to zero}
END EXEC[19]
BEGIN EXEC[20]
Killed {msg: Memory WIP: TODO: load from device memory ==> PV(Prov_device, PVfromint(IVop(-, IVop(rem_f, IVop(+, IVfromptr(signed int, uintptr_t, PVbase(4, {main.x}), [SPE_array(signed int,IVconcrete(0))]), IVop(-, IVop(rem_f, IVop(-, IVop(rem_f, IVop(-, IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(1))]), IVfromptr(signed int, uintptr_t, PVbase(3, {main.y}), [SPE_array(signed int,IVconcrete(0))])), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616))), IVconcrete(18446744073709551616)), IVconcrete(18446744073709551616))), [])}
END EXEC[20]
BEGIN EXEC[21]
Killed {msg: Memory WIP: tried to cast to a pointer type an (non device) integer value non-equal to zero}
END EXEC[21]
Time spent: 0.593026 seconds
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 x[1]=11 *p=11
Conversion from an integer to non-null pointer:
> in main at pointer_arith_algebraic_properties_2_auto.c:5: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

ch2o pointer_arith_algebraic_properties_2_auto.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_local]-->
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_local]-->
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_local]-->
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_auto.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.