Re:Chad Strings – The Chad way to handle strings in C
by quotemstr on Friday May 21, 2021 @03:08AM
(#27231297)
> C++ verifiers have to understand template types, overloads, etc.
If they operate at some compiler IR level (e.g. LLVM bitcode), the difference between C and C++ verification is nothing. C++ is purely a front-end thing. Why should formal verifiers operate at the AST level?
I'm sure we'll get there one day. Frama-C is inching toward it at molasses speeds.
But right now, C is undeniably easier to verify than C++.