Использование двоичных констант (префикс 0b) в коде, обработанном Splint

Question

Согласно веб-сайту GCC и Руководству SDCC_§3.5.5, и GCC, и SDCC допускают использование двоичных констант, таких как эта, где представлено десятичное число 2: 0b0010

К сожалению, splint, кажется, не справляется с этим хорошо, что приводит к ошибке разбора, как показано ниже.

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

Выход

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