Linux Driver Verification

Unfortunately, in compiling kernels with a new compiler like gcc 4.6.0 on which aspectator is based, we obtain constructions that cannot be parsed by CIL. For instance, in arch/x86/include/asm/cpufeature.h we have:

#if __GNUC__ > 4 || __GNUC_MINOR__ >= 5
        asm goto(... : : "i" (bit) : : t_no);
        return true;
    t_no:
        return false;
#else
        u8 flag;
        asm volatile(... : "=qm" (flag) : "i" (bit));
        return flag;
#endif

that leads to:

ZZZ: Exception: Frontc.ParseError("Parse error") 
.../inst/current/envs/linux-2.6.37/linux-2.6.37/arch/x86/include/asm/cpufeature.h[321:0-0] : syntax error Parsing error
Ack! The gremlins again!: Frontc.ParseError("Parse error") 
Fatal error: exception Frontc.ParseError("Parse error")

Possible ways of solution:

1. Use options like for llvm aspectator that will prevent such constructions (the simplest way)
2. Add some simplifications to C backend, e.g. to skip all 'asm goto's (it's harder)
3. Add support of 'asm goto' to CIL (the hardest way)