We found the following two bugs during our proof of separate compilation.

#1. A bug that occurs only in the presence of linking

Here is a counter example due to this bug.

    // a.c
    #include <stdio.h>
    int x;
    extern int* const xptr;
    int main() {
        x = 1;
        *xptr = 0;
        // correct: 0, actual: 2
        printf("%d\n", x + x);
        return 0;
    }

    // b.c
    #include <stdio.h>
    extern int x;
    int* const xptr = &x;

If you compile this using CompCert 2.4, it prints out “2” though it should print “0”. The reason for this bug is that the read-only-memory analysis is not correct in the presence of linking. This bug was reported to Xavier Leroy, and patched in the main CompCert repository. For more details, see §4.1 of our paper.

#2. A bug that occurs even in the absence of linking

    #include <stdio.h>
    long long __i64_dtos(float t) {
        return 3;
    }
    int main() {
        // correct: 5, actual: 3
        printf("%lld\n", (long long) 5.0f);
        return 0;
    }

If you compile this using CompCert 2.4, it prints out “3” instead of “5”. The reason for this bug is that one of the axioms assumed is not true. More specifically, the function get_helpers does not satisfy the following axiom:

    Axiom get_helpers_correct:
      forall ge hf, 
        get_helpers ge = OK hf -> 
        i64_helpers_correct ge hf.

This bug was reported to Xavier Leroy, and patched in the main CompCert repository. For more details, see §5.2 of our paper.