Using Binary Constants (prefix 0b) In Code Processed by Splint

Question

According to the GCC website and the SDCC Manual_§3.5.7, both GCC and SDCC allow the use of binary constants such as this one, where the decimal number 2 is represented: 0b0010

Unfortunately, splint does not seem to handle this well resulting in a parse error, as shown below.

binaryConstants.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;                                        
}

Output

$ 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.
$

Output with +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.
$

Is there a flag to allow this extension to C?