2 ms·
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
by rurban 2y ago
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__
- gergo_barany 2y ago__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