Comment by 1718627440
9 hours ago
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.
By "static analysis" you mean unsound, best-effort analyzers which try to study code as-is, rarely allow extra annotations, and tolerate false negatives and even positives by design.
While these are a huge improvement over no extra tooling, they don't compare to analyzers like Frama-C plugins, which demand further annotations/proofs if necessary to show code is free of UB, and you can provide further to show your code is not just safe, but correct. Assuming one doesn't ship rejected code, the latter is pretty much its own language with much stronger guarantees, much like SPARK is to Ada.
I like sanitizers and other compiler-specific guarantees, they at least try to fill the gaps by giving proper semantics to UB. But the ones available for C are still insufficient, and some are very resource-heavy compared to just running safe code. I'm excited about Fil-C showing a path forward here.
Yes, I do. I know they are very different from real correctness verifiers, but it's not like the people only using the compiler has no way of preventing trivial UB bugs. UB also is really only a language concept and nobody is writing code for the abstract C machine.