What subset of C is supported by Verifiable-C?

Question

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?

Answer 1

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.

Answer 2

Verifiable C manual (see page 9) states that the instrument works with subset of C with number of restrictions. But clightgen tool that comes with CompCert installation translates C into CompCert’s Clight intermediate language, so the subset with which Verifiable C can work is almost entire C.