4376 goto ldv_20876;
4377 } else
4378#line 458
4379 if (ldv_s_pm_drv_serio_driver != 0) {
4380#line 460
4381 goto ldv_20876;
4382 } else {
4383#line 462
4384 goto ldv_20878;
4385 }
4386 ldv_20878: ;
4387 ldv_module_exit:
4388 {
4389#line 551
4390 pm_exit();
4391 }
4392 ldv_final:
4393 {
4394#line 554
4395 ldv_check_final_state();
4396 }
4397#line 557
4398 return;
4399}
4400}
4401#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3116/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4402void ldv_blast_assert(void)
4403{
4404
4405 {
4406 ERROR: ;
4407#line 6
4408 goto ERROR;
4409}
4410}
4411#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3116/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4412extern int __VERIFIER_nondet_int(void) ;
4413#line 578 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3116/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/penmount.c.p"
4414int ldv_spin = 0;
4415#line 582 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3116/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/penmount.c.p"
4416void ldv_check_alloc_flags(gfp_t flags )