6229 goto ldv_20978;
6230 } else
6231#line 791
6232 if (ldv_s_w8001_drv_serio_driver != 0) {
6233#line 793
6234 goto ldv_20978;
6235 } else {
6236#line 795
6237 goto ldv_20980;
6238 }
6239 ldv_20980: ;
6240 ldv_module_exit:
6241 {
6242#line 944
6243 w8001_exit();
6244 }
6245 ldv_final:
6246 {
6247#line 947
6248 ldv_check_final_state();
6249 }
6250#line 950
6251 return;
6252}
6253}
6254#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3129/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6255void ldv_blast_assert(void)
6256{
6257
6258 {
6259 ERROR: ;
6260#line 6
6261 goto ERROR;
6262}
6263}
6264#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3129/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6265extern int __VERIFIER_nondet_int(void) ;
6266#line 971 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3129/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/wacom_w8001.c.p"
6267int ldv_spin = 0;
6268#line 975 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3129/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/wacom_w8001.c.p"
6269void ldv_check_alloc_flags(gfp_t flags )