Search code examples
cverifiable-c

What subset of C is supported by Verifiable-C?

I'm trying to figure out what subset of C is supported by Verifiable C from Verified Software Toolchain. "Program Logics For Certified Compilers" (p. 143) states that it is subset of Clight. But CompCert compiler transforms program from CompCert C to Clight. Does that mean that it is possible to verify any CompCert C program by Verifiable C?

Solution

  • Indeed, using Verifiable C one first uses CompCert's parser/typechecker to transform C into Clight, so it's not really about "What's in C but not in Clight", it really is about "which features of C are not supported." Page 9 of the reference manual says, basically:

    • Goto is not supported in Verifiable C (but CompCert supports goto).
    • Struct-copy (by struct assignment, struct parameters) is not supported in Verifiable C (but I think it's supported in CompCert)
    • Only structured switch statements (no Duff's device in either VC or CompCert)
    • Can't cast pointers to integers then do arithmetic on the result.

    Those are the main limitations.