Giving C a superpower: custom header file (safe_c.h)

I don't understand this passion for turning C into what it's not...

Just don't use C for sending astronauts in space. Simple.

C wasn't designed to be safe, it was designed so you don't have to write in assembly.

Just a quick look through this and it just shows one thing: someone else's walled garden of hell.

> Just don't use C for sending astronauts in space

But do use C to control nuclear reactors https://list.cea.fr/en/page/frama-c/

It's a lot easier to catch errors of omission in C than it is to catch unintended implicit behavior in C++.

I 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.

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.