Linux Driver Verification

For all drivers RCV prints in its log:

...
include/linux/rcupdate.h:432: Error: Cannot resolve variable rcu_lock_map. 
include/linux/rcupdate.h:432: Error: Expected lval for ADDROF. Got Const(Int64(0,int,None)) 
include/linux/rcupdate.h:917: Warning: CALL in constant
include/linux/rcupdate.h:917: Error: Length of array is negative
include/linux/rcupdate.h:920: Warning: CALL in constant
include/linux/rcupdate.h:920: Error: doPureExp: not pure
...

The first issue seems to be connected with incorrect manual kernel configuring. We unset CONFIG_DEBUG_LOCK_ALLOC and CONFIG_PROVE_LOCKING, but don't touch CONFIG_PROVE_RCU, that in fact depends on CONFIG_PROVE_LOCKING. So, I guess that solution is to turn off CONFIG_PROVE_RCU.
The second issue comes from:

BUILD_BUG_ON(!__builtin_constant_p(offset));

that becomes after preprocessing:

((void)sizeof(char[1 - 2*!!(!__builtin_constant_p(offset))]));

That also is a problem for aspect models:

In file included from include/linux/rculist.h:10:0, from include/linux/dcache.h:6, from include/linux/fs.h:387, from include/linux/tty.h:39, from /ldv/launch/work/current--X--drivers/usb/serial/kobil_sct.ko--X--defaultlinux--X--100_1a/linux/csd_deg_dscv/11/dscv_tempdir/dscv/ri/100_1a/drivers/usb/serial/kobil_sct.c.p:2: 
include/linux/rcupdate.h: In function '__kfree_rcu': 
include/linux/rcupdate.h:917:2: error: size of unnamed array is negative

Looks like 3.4 kernel isn't intended for build... __kfree_rcu function body is unconditional. May be just configure BUILD_BUG_ON in some way.