The kcc compiler is really good at being predicatable. A formal semantics of the language gives warnings whenever undefined behavior occurs.

https://github.com/kframework/c-semantics