Daniel Dickman
Daniel Dickman
with gcc: ``` $ cat foo.c #include void foo(void) { puts("Hello Shared World"); } $ gcc -fpic -std=c99 -c foo.c $ gcc -shared -o libfoo.so foo.o $ ``` with CompCert...
In my build system, gcc takes input from stdin like below. It would be nice if CompCert allowed the same thing. Of course, the code on my end can be...
gcc allows basic asm blocks outside of any function: ``` $ cat foo.c asm("cli"); int main() { return 1; } $ gcc foo.c ``` compcert, doesn't seem to support this:...
### Describe the issue: Starting with numpy 1.20rc1 and also happening in every release through 1.22.0, the tests cause a segfault on OpenBSD/i386. I've tested this with both python 3.8...
It would be really great to support the +r constraint in extended asm. For example to support this code: https://github.com/openbsd/src/blob/b3424f948f9275685df5315a2922aad768594479/sys/arch/amd64/include/endian.h#L44 If support is not possible then this type of code...
Currently if an unrecognized warning is passed to CompCert, the compiler will error out. Clang will print a warning (they have a -Wunknown-warning-option) and continue compilation. I’d like to request...
On newer Intel x86/64 CPUs and on OpenBSD, CompCert produced binaries will crash due to lack of IBT support. As a quick solution we can append “-z nobtcfi” to clinker_options...