1. 3

Abstract: “Test coverage is often measured by the number of source lines of code that is executed by tests. However, compilers can apply transformations to the code to optimize the performance or size of a program. These transformations can remove parts of the original code, but they can also add new code by creating specialized copies and additional conditional branches. This means that while at source code level it seems as if all code would be tested, it is quite possible that the actually executed machine code is only partially tested. This project investigates how confidence in the correctness of a compiler’s opti- mizations can be improved. To this end we create a suite of programs that explicitly trigger compiler optimizations and test their correctness with coverage on machine code level. Once confidence into the correctness of the compiler has been established, it becomes sufficient to test application software with high source code coverage only.”

  1.  

  2. 1

    @derek-jones, thought you might find this interesting. Also, a press release says Solid Sands will apply or has applied its test suit to CompCert. That was 2018. This paper references an error in CompCert they submitted before the press release. I emailed Solid Sands asking what the results were. No reply yet. I haven’t emailed AbsInt since I think they’d be too biased.

    1. 2

      Thanks. The title didn’t ring any bells. Then I read it, nothing to see here.

      This paper is much more interesting.