3 ms·
First I stumbled upon Xr0, and now this! I really enjoy these attempts at safe C. Kinda wish I didn't have to recompile this myself though. But the procedure do
by Alifatisk 2y ago
First I stumbled upon Xr0, and now this! I really enjoy these attempts at safe C. Kinda wish I didn't have to recompile this myself though. But the procedure doesn't look that challenging anyways.
- naasking 2y agoCompCert isn't about a safe C, it's a verified C compiler. This means it has proofs that verify that the compiler correctly implements the C standard and that the binary code it produces is a faithful implementation of the original program as determined by C's semantics. This is used, for example, as part of the verification for the high-integrity, high-security seL4 microkernel.
- Alifatisk 2y agoOhhh okey!