__FILE__ and __LINE__ are not extensions, they are standard C constructs. They are typically resolved by the preprocessor, just like #include and whatever, so t

__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 https://gcc.godbolt.org/z/E8sMPPTs4