3 ms·

From CompCert site: "What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs,

by feider 11y ago

From CompCert site: "What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues." I'm not very into C language - what are these miscompilation issues? What is the practical impact that CompCert C brings?

witty_username 11y ago
Miscompilation issues means bugs in the compiler causing incorrect assembly to be generated.
- feider 11y ago
  I understood that. Sorry if my question was bit unclear. What I wanted to know was _specifically_ what these bugs are / what causes them / what is practical impact (i.e. probability of application crashing or other serious event due to use of GCC etc)
  - sanxiyn 11y ago
    Check out "Finding and Understanding Bugs in C Compilers": http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf. The paper explains what-is-bug/what-causes-it/what-is-impact for selected bugs. Complete list of 282 compiler bugs found (79 GCC, 203 LLVM) is also available online: http://embed.cs.utah.edu/csmith/ http://embed.cs.utah.edu/csmith/.
    - feider 11y ago
      Thank you, that paper seems to be surprisingly easy to read (being an academic paper that is).
  - nickpsecurity 11y ago
    Especially see the CompCert section on page 6 of the Csmith PDF to see what a difference formal verification made. Note that compilers don't have to go that far: typed, functional, thoroughly-tested code in something like Ocaml or Haskell can achieve 80-90% of that quality with relatively little effort. Hence, why I promote rewriting and further extending things like LLVM in languages like ML, Ada, or Eiffel that support advanced checks.