Ferrocene released as open source

Posted Oct 11, 2023 18:33 UTC (Wed) by DemiMarie (subscriber, #164188)
In reply to: Ferrocene released as open source by farnz
Parent article: Ferrocene released as open source

This doesn’t (or at least shouldn’t) actually work, because UB is a global property of the execution of a program: as soon as execution is guaranteed to have UB, it has no meaning at all. That alerting code could reboot the brake controller or cause arbitrary memory corruption.

Ferrocene released as open source

Posted Oct 12, 2023 0:03 UTC (Thu) by NYKevin (subscriber, #129325) [Link] (1 responses)

That is not a contradiction. The compiler's certification can be more demanding than the C standard. It can also require you to pass specific compiler flags (such as -O0) and only certify that the compiler behaves "correctly" with those flags.

Ferrocene released as open source

Posted Oct 12, 2023 10:27 UTC (Thu) by farnz (subscriber, #17727) [Link]

And for the qualified constructs, you're already in a subset of C where certain rules must be followed, ensuring that the UB has to be outside the part of code that's certified. From the compiler's point of view, there's a clear boundary between certifiable C and plain standards C - the first code it encounters that's not following the qualification rules is the boundary between the two.

A compiler could therefore choose to split the program into two at that point; indeed, some qualified toolchains require code that's going to be certified to be in separate translation units (TUs) to general code, and require you to tell it which TUs are going to be certified; it can then avoid cross-TU optimization between code that's going to be certified (and hence will have any UB caught by code audit) and code that's just going to be compiled and linked into the program.