alt Hacker NewsI consider code written in Frama-C as a verifiable C dialect, like SPARK is to Ada, rather than C proper. I find it funny how standard C is an undefined-behaviour minefield with few redeeming qualities, but it gets some of the best formal verification tools around.
Replies
uecker • yesterday at 6:28 PM
IMHO and maybe counterintuitively, I do not think the existence of UB makes it harder to do formal verification or have safe C implementations. The reason is that you can treat it as an error if the program encounters UB, so one can either derive local requirements or add run-time checks (such as Fil-C) and then obtains spatial and temporal isolation of memory object.
The popular C compilers include a static analyzer and a runtime sanitizer. What features do you consider proper C? The C standard has always been about standardization of existing compilers, not about prescribing features.