c - 在 Splint 处理的代码中使用二进制常量（前缀 0b）

Question

根据GCC 网站和SDCC 手册_§3.5.7，GCC 和 SDCC 都允许使用二进制常量，例如这个，其中十进制数 2 表示：0b0010

不幸的是，夹板似乎不能很好地处理这个导致解析错误，如下所示。

二进制常量.c

#include <stdio.h>                                       
int main(){                                              
        int one = 0b0001;                                
        int two = 0x2;                                   
        int three = 3;                                   
        printf("B: %d\nH: %d\nD: %d\n", one, two, three);
        return 0;                                        
}

输出

$ splint binaryConstants.c
Splint 3.1.2 --- 19 Oct 2016

binaryConstants.c:3:18: Parse Error. (For help on parse errors, see splint -help
               parseerrors.)
*** Cannot continue.
$

使用 +gnuextensions 输出

$ splint +gnuextensions binaryConstants.c
Splint 3.1.2 --- 19 Oct 2016

Command Line: Setting +gnuextensions redundant with current value
binaryConstants.c:3:18: Parse Error. (For help on parse errors, see splint -help
                 parseerrors.)
*** Cannot continue.
$

是否有允许将此扩展到 C 的标志？