CompCert puts constants in the text segment, which breaks under operating systems (e.g. OpenBSD) that make it execute-only

[monniaux]

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.

[xavierleroy]

Should be fixed by a899ced. Thanks for the report.