Some caveats in this compiler: "In C source files, attribute qualifiers can occur anywhere a standard type qualifier (const, volatile) can occur, and also just

Some caveats in this compiler: "In C source files, attribute qualifiers can occur anywhere a standard type qualifier (const, volatile) can occur, and also just after the struct and union keywords. For partial compatibility with GCC, the CompCert parser allows attributes to occur in several other places, but may silently ignore them. Warning. Some standard C libraries, when used in conjunction with CompCert, deactivate the __attribute__ keyword: the standard includes, or CompCert itself, define __attribute__ as a macro that erases its argument. This is the case for the Glibc standard library under Linux, and the Xcode header files under macOS. For this reason, please use the __attribute keyword in preference to the __attribute__ keyword." I learned C in the 80's and did a lot of it for about 10 years. After not doing much software development for another 10 years or so, I wrote an embedded OS and an application (for the MSP430 platform). I was surprised by the advances in compiler optimization while I had been away. I needed to be much more diligent when interacting with hardware and locking. (E.g. Use the volatile qualifier generously, or my code would not work.) I also found some odd compiler bugs (in the TI compiler) related to bit fields.