[Mathnerd314]

For more, see https://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_20... (clearly distinguishing C* which corresponds to the hardware from "C" which is the subset of C* that excludes all undefined behaviour) and https://arxiv.org/pdf/2201.07845.pdf "How ISO C became unusable for operating systems development".