Example: pointer_from_concrete_address_1.c

int main() { 
  // on systems where 0xABC is not a legal non-stack/heap 
  // address, does this have undefined behaviour?
  *((int *)0xABC) = 123;
}

Experimental data (what does this mean?)

gcc-8.1-O0
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

gcc-8.1-O2
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

gcc-8.1-O3
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

gcc-8.1-O2-no-strict-aliasing
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

gcc-8.1-O3-no-strict-aliasing
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

clang-6.0-O0
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

clang-6.0-O2
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

clang-6.0-O3
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

clang-6.0-O2-no-strict-aliasing
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

clang-6.0-O3-no-strict-aliasing
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

clang-6.0-UBSAN
 
exit codes: compile 0 / execute 1
UndefinedBehaviorSanitizer:DEADLYSIGNAL
==23529==ERROR: UndefinedBehaviorSanitizer: SEGV on unknown address 0x000000000abc (pc 0x000000420c30 bp 0x000000420c40 sp 0x7ffca18e82a8 T23529)
==23529==The signal is caused by a WRITE memory access.
==23529==Hint: address points to the zero page.
    #0 0x420c2f  (/auto/homes/vb358/charon2/pointer_from_concrete_address_1.c.clang-6.0-UBSAN.out+0x420c2f)
    #1 0x7f523777382f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #2 0x402988 in _start (/auto/homes/vb358/charon2/pointer_from_concrete_address_1.c.clang-6.0-UBSAN.out+0x402988)

UndefinedBehaviorSanitizer can not provide additional info.
==23529==ABORTING

clang-6.0-ASAN
 
exit codes: compile 0 / execute 1
AddressSanitizer:DEADLYSIGNAL
=================================================================
==23543==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000abc (pc 0x0000004e71cc bp 0x0000004e7200 sp 0x7ffd78613180 T0)
==23543==The signal is caused by a WRITE memory access.
==23543==Hint: address points to the zero page.
    #0 0x4e71cb in main (/auto/homes/vb358/charon2/pointer_from_concrete_address_1.c.clang-6.0-ASAN.out+0x4e71cb)
    #1 0x7f800a43082f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #2 0x419d78 in _start (/auto/homes/vb358/charon2/pointer_from_concrete_address_1.c.clang-6.0-ASAN.out+0x419d78)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (/auto/homes/vb358/charon2/pointer_from_concrete_address_1.c.clang-6.0-ASAN.out+0x4e71cb) in main
==23543==ABORTING

clang-6.0-MSAN
 
exit codes: compile 0 / execute 77
MemorySanitizer:DEADLYSIGNAL
==23558==ERROR: MemorySanitizer: SEGV on unknown address 0x000000000abc (pc 0x00000048db10 bp 0x00000048db40 sp 0x7ffca9196bb8 T23558)
==23558==The signal is caused by a WRITE memory access.
==23558==Hint: address points to the zero page.
    #0 0x48db0f in main (/auto/homes/vb358/charon2/pointer_from_concrete_address_1.c.clang-6.0-MSAN.out+0x48db0f)
    #1 0x7f3b0a47d82f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #2 0x41a6d8 in _start (/auto/homes/vb358/charon2/pointer_from_concrete_address_1.c.clang-6.0-MSAN.out+0x41a6d8)

MemorySanitizer can not provide additional info.
SUMMARY: MemorySanitizer: SEGV (/auto/homes/vb358/charon2/pointer_from_concrete_address_1.c.clang-6.0-MSAN.out+0x48db0f) in main
==23558==ABORTING

icc-19-O0
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

icc-19-O2
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

icc-19-O3
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

icc-19-O2-no-strict-aliasing
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

icc-19-O3-no-strict-aliasing
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

cerberus-concrete
 
BEGIN EXEC[0]
Defined {value: "Specified(0)", stdout: "", blocked: "false"}
END EXEC[0]
Time spent: 0.011840 seconds

cerberus-symbolic
 
BEGIN EXEC[0]
Defined {value: "Specified(0)", stdout: "", blocked: "false"}
END EXEC[0]
BEGIN EXEC[1]
Killed {msg: Memory WIP: tried to cast to a pointer type an (non device) integer value non-equal to zero}
END EXEC[1]
Time spent: 0.029738 seconds

gcc-4.9-shadowprov
 
exit codes: compile 0 / execute 139

CHERI:MIPS-O0
 
exit codes: compile 0 / execute -1
Terminated with signal 11: Segmentation fault
CHERI:MIPS-O2
 
exit codes: compile 0 / execute -1
Terminated with signal 11: Segmentation fault
CHERI:MIPS-O2-no-strict-aliasing
 
exit codes: compile 0 / execute -1
Terminated with signal 11: Segmentation fault
CHERI:CHERI-O0-uintcap-addr-exact-equals
 
exit codes: compile 0 / execute -1
Terminated with signal 34: In-address space security exception
CHERI:CHERI-O2-uintcap-addr-exact-equals
 
exit codes: compile 0 / execute -1
Terminated with signal 34: In-address space security exception
CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr-exact-equals
 
exit codes: compile 0 / execute -1
Terminated with signal 34: In-address space security exception
CHERI:CHERI-O0-uintcap-offset-exact-equals
 
exit codes: compile 0 / execute -1
Terminated with signal 34: In-address space security exception
CHERI:CHERI-O2-uintcap-offset-exact-equals
 
exit codes: compile 0 / execute -1
Terminated with signal 34: In-address space security exception
CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset-exact-equals
 
exit codes: compile 0 / execute -1
Terminated with signal 34: In-address space security exception
CHERI:CHERI-O0-uintcap-addr
 
exit codes: compile 0 / execute -1
Terminated with signal 34: In-address space security exception
CHERI:CHERI-O2-uintcap-addr
 
exit codes: compile 0 / execute -1
Terminated with signal 34: In-address space security exception
CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr
 
exit codes: compile 0 / execute -1
Terminated with signal 34: In-address space security exception
CHERI:CHERI-O0-uintcap-offset
 
exit codes: compile 0 / execute -1
Terminated with signal 34: In-address space security exception
CHERI:CHERI-O2-uintcap-offset
 
exit codes: compile 0 / execute -1
Terminated with signal 34: In-address space security exception
CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset
 
exit codes: compile 0 / execute -1
Terminated with signal 34: In-address space security exception
RV-Match
 
exit codes: compile 0 / execute 1
pointer_from_concrete_address_1.c:4: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
 
Fatal error: exception Main.CH2O_error("cast or initializer cannot be typed")
Raised at file "map.ml", line 117, characters 16-25
Called from file "str.ml", line 253, characters 6-29

compcert-3.2
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

compcert-3.2-O
 
exit codes: compile 0 / execute 139
Segmentation fault (core dumped)

compcert-3.2-interp
 
Time 0: calling main()
--[step_internal_function]-->
Time 1: in function main, statement *((int *) 2748) = 123; return 0;
--[step_seq]-->
Time 2: in function main, statement *((int *) 2748) = 123;
--[step_do_1]-->
Time 3: in function main, expression *((int *) 2748) = 123
--[red_cast]-->
Time 4: in function main, expression *2748 = 123
Stuck state: in function main, expression *2748 = 123
Stuck subexpression: *2748
ERROR: Undefined behavior