3 ms·
On that note: what even is a correct translation of C when it has so many undefined behaviors in it's spec.
by Avshalom 12y ago
On that note: what even is a correct translation of C when it has so many undefined behaviors in it's spec.
- wmf 12y agoWhat if the code doesn't rely on undefined behavior?
- regehr 12y agoAbsence of undefined behavior in the C implementation is of course one of the things covered by the seL4 proof.
- cc_ 12y agoThey use a formally-specified subset of C described in Harvey Tuch's PhD thesis: http://www.ssrg.nicta.com.au/publications/papers/Tuch:phd.pdf http://www.ssrg.nicta.com.au/publications/papers/Tuch:phd.pd...