Note that this formalization is substantially incomplete: check page 195. CH2O does not formalize variadic function, float, bit field, setjmp/longjmp. All of them are formalized in KCC.
There are a few real gems in this thesis. In particular, I really liked the explanation of sequence points in terms of separating conjunction. This is much more compact than the imperative program to decide definedness that is implicitly described in the C standard.
The proofs of equivalence between the different semantic descriptions also go beyond what KCC does, or for that matter what you can do within the K framework (at the moment).
CH2O's main innovation is C standard (as opposed to C implementation) formalized in general purpose prover (as opposed to custom system). KCC formalized C standard, but not in general purpose prover. CompCert formalized in general purpose prover, but formalized implementation instead of standard.
Formalizing in general purpose prover is useful because you can use all of math to prove runtime invariants. But if you want to prove runtime invariants, you usually want to prove with respect to concrete implementation, not to prove abstractly to standard. For time when you want to prove abstractly to standard, this doesn't seem better than KCC.
In short, this feels like Not Invented Here against KCC. Probably unfair characterization, but that's what it feels to me.
That's where I'd go. Extending KCC to do what a theorem prover could seems more challenging.
"For time when you want to prove abstractly to standard, this doesn't seem better than KCC. In short, this feels like Not Invented Here against KCC. Probably unfair characterization, but that's what it feels to me."
The obvious interpretation is commenter thinking KCC is better and (see NIH) the OP should've maybe done something with it instead...?
" Another comment points out following the standard is good for portabilities sake. Somehow, that all seems obvious to me."
You can follow the standard and be portable if you keep certain parts as options subject to interpretation/choice of the implementers. That's the so-called undefined behavior mostly.
Really? I would think that if you're trying to write a portable program, it would be much more useful to prove invariants based on the language specification, not a particular concrete implementation.