I wonder how many projects actually do use ccert in its pipeline. I've tried on some big library of mine (25Mb compiled), but it usually runs out of memory. And it's a hassle to fix all the extensions which ccert doesn't support. Esp. __FILE__ and __LINE__
__FILE__ and __LINE__ are not extensions, they are standard C constructs. They are typically resolved by the preprocessor, just like #include and whatever, so the actual CompCert compiler should never see them. Maybe you're doing something weird, applying it to non-preprocessed files in a mode where it thinks the input is already preprocessed?
EDIT: In fact, here is CompCert preprocessing and then compiling a file containing __FILE__ and __LINE__ just fine: https://gcc.godbolt.org/z/E8sMPPTs4
