Hacker News new | comments | show | ask | jobs | submit login

One can use clang and gcc to either produce a runtime error if undefined behaviour is detected or that and abort the program.

There are several things, like signed overflow of integrals, that cannot often be determined at compile time.

I think the OP is referring to full-blown verification systems, like some dependently typed languages have (although they aren't the only ones). If your program's behavior is defined because you wrote it that way (i.e. not by chance), you would have an argument for why the undefined behavior is not invoked that could be translated into a formal proof in most sophisticated (i.e. ZFC-ish) formal systems.

Formal verification, yes. Mechanical verification (dependent types, SAT/SMT solvers, model checkers, etc.), not necessarily. I don't mean to insult the efforts of the mechanical verification community, but it's preposterous to suggest that the only way to verify programs is to use a computer. Hey, we have brains! We can use them too!

To my knowledge the undefined behavior sanitizers are not complete. It is also unclear how you both optimize your program (exploiting undefined behavior semantics) and providing a runtime check without completely killing performance.

Use it during your unit tests, clang claims the runtime cost is small so it might now matter either.

As useful as debugging tools are, they are no replacement for design tools.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | DMCA | Apply to YC | Contact