2 ms·
> C can be verified quite easily. C++ cannot. Uh, exactly the same kind of static analysis that applies to C applies just as well to C++. C++ doesn't have a ma
by quotemstr 5y ago
> C can be verified quite easily. C++ cannot.
Uh, exactly the same kind of static analysis that applies to C applies just as well to C++. C++ doesn't have a magically different execution model. What do you think std::string is except a few wrapper functions that boil down to the same operations you can do in C?
- junon 5y agoNote the term "easily". C++ verifiers have to understand template types, overloads, etc. 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++.
- quotemstr 5y ago> 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?