By default, debug builds of seL4 compiled with the standard CMake scripts are compiled with optimization on as well as debugging symbols. This has made debugging some code I’ve been working on harder than it would be if it was unoptimized. However, when I go in and disable optimization by setting the build type from RelWithDebInfo to Debug in CMakeFiles.txt and adding a “-O0” compiler flag, seL4 crashes during boot at unexpected locations.
Is there a reason seL4 is compiled optimized when debugging? I know the Linux kernel has issues with being compiled unoptimized in any situation (in part due to inlining) and it is considered an unsupported option. (Alternately, this could be an issue with my environment/codebase.)