🚀 go-pugleaf

Michel asks:

"If the language allows arbitrary pointer arithmetic or even explicit
"free" of dynamically allocated memory, you cannot "rigorously" check
everything. This is why you see so many competing products to check C
programs. None does a thorough job although some are quite good.
If you are willing to subset the portion of the language that you are using
then you can garantee safety."

You can in fact rigorously check everything against the ANSI standard, but
only by keeping additional runtime data strucures (as for instance Purify
does). Furthermore, most C programmers would not want such rigorous
checking because it would forbid things which in practice work fine on
all C compilers.

It is a common position to say that C (and other languages without bounds
checking built-in, like Fortran or COBOL) are equivalent to Ada since
bounds checking is simply an implementation matter, but it is an
incorrect one. There is in practice a big diffrerence between a language
like Ada, where bounds checking is part of the sematncis and the language
is designed so that it is easy to implement, and the assumption is that the
default is checks on, and a language where you can implement limited
bounds checking, but not easily, and certainly you would not expect to
see it as the default.