News for hackers. Stuff that matters.

A comment on The Case for Formal Verification (2013). Parent comment

Re:The Case for Formal Verification (2013) by ahomescu1 on Sunday April 20, 2014 @06:12PM (#7618671)
It doesn't support all of C99 [1]. In real-world code, you need that, plus the GNU extensions (the clang developers put in a lot of work into making clang fully compatible with gcc, going as far as accepting the same command-line switches).

1 - http://compcert.inria.fr/compcert-C.html#subset

[ Parent | on HN ]
Re:The Case for Formal Verification (2013) by nullc on Sunday April 20, 2014 @07:26PM (#7618872)
Considering that the parts of C99 that it doesn't support are also not supported by MSVC I can't imaging that that alone is much of a big deal.

The prohibition on commercial use is a much bigger barrier, I expect.

[ Parent | on HN ]
Re:The Case for Formal Verification (2013) by ahomescu1 on Sunday April 20, 2014 @09:16PM (#7619191)
MSVC supports C++ instead (AFAIK, it has most of C++11 implemented), while CompCert doesn't compile C++ at all.
[ Parent | on HN ]