I presume that KCC in question is https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics, i.e., a formalization of C programming la

I presume that KCC in question is https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics, i.e., a formalization of C programming language in a form suitable for evaluation. It indeed can detect undefined behaviour, though last time I played with it (a few years ago) it was hardly something that you can use on anything but trivial examples. Not to mention that it crashed on various implementation defined behaviours (for example comparing unrelated pointers with <) limiting its usefulness even further. BTW, both gcc and clang contain runtime checker for easily detectable undefined behaviours like singed overflow you have mentioned. You can enable it with -fsanitize=undefined.