Certain operating systems set the text segment execute-only as a security measure. This is most notably the case by default with OpenBSD on x86-64, AArch64, MIPS64, PowerPC32, PowerPC64, RISC-V, and SPARC64.
CompCert stores certain constants in the text segment. This is for instance the case of jump tables and two floating-point constants in __compcert_i64_dtou on x86-64. This breaks under those operating systems.
A workaround on OpenBSD is to assemble and link using cc -Wl,--no-execute-only.
I'm unsure of the implications of storing these constants in .rodata as opposed to .text.
Certain operating systems set the text segment execute-only as a security measure. This is most notably the case by default with OpenBSD on x86-64, AArch64, MIPS64, PowerPC32, PowerPC64, RISC-V, and SPARC64.
CompCert stores certain constants in the text segment. This is for instance the case of jump tables and two floating-point constants in
__compcert_i64_dtouon x86-64. This breaks under those operating systems.A workaround on OpenBSD is to assemble and link using
cc -Wl,--no-execute-only.I'm unsure of the implications of storing these constants in
.rodataas opposed to.text.