3 ms·

Testing compiler outputs by testing popular libraries an apps generated with it is a fine and common approach. Expecting a compiler (and the hardware it runs o

Testing compiler outputs by testing popular libraries an apps generated with it is a fine and common approach. Expecting a compiler (and the hardware it runs on) to be perfect is a mistake.

thechao 6y ago
Except for compcert, which is basically perfect.
- jraph 6y ago
  Well, not quite, because there are parts of CompCert that are not proven [1]: - Parsing, type-checking, and pre-simplifications - Assembling and linking And there have been bugs on edge cases there. Moreover, correctness is limited to what is specified. COQ does not guarantee that there are no missing specifications or theorems. The C standard is written in English, people had to manually encode the standard in COQ. [1] http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html
  - touisteur 6y ago
    And the performance of the generated binary might be underwhelming for some.
cesarb 6y ago
It's all right if it's running the testcases of these popular libraries; however, it seems that this was not caught by the testcases, only by a fuzzer (which not only is not as deterministic, but also can be much more costly to run).