4 ms·

Does anybody know how does this compare to https://compcert.org/ https://compcert.org/ ?

• ryao 4y ago
  It does not. One is a language extension that claims to prevent certain classes of issues. The other is a C compiler that claims to do nothing to prevent those classes of issues. The two are not comparable at all. You would be better off comparing it to Astree, which is a static analyzer written by the group that wrote the Compcert C compiler. https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm Astree claims to be able to prove the absence of use-after-free, which the checked C documentation says that checked C does not prevent. You would need to check to see if Astree can prove the absence of all of the issues that checked C is intended to prevent, but at a glance that seems possible. In theory, Astree can be used to fix all of them by doing fixes until it stops complaining.
  • ryao 4y ago
    > You would be better off comparing it to Astree, which is a static analyzer written by the group that wrote the Compcert C compiler. I was wrong to write this. They were written by different groups in France, but licenses for both of them are being sold by the same company, which made it easy to mistake the creators as the same group. I realized my misunderstanding several hours after making that comment and could not edit to correct the error.