3380 goto ldv_20796;
3381 } else
3382#line 346
3383 if (ldv_s_warrior_drv_serio_driver != 0) {
3384#line 348
3385 goto ldv_20796;
3386 } else {
3387#line 350
3388 goto ldv_20798;
3389 }
3390 ldv_20798: ;
3391 ldv_module_exit:
3392 {
3393#line 427
3394 warrior_exit();
3395 }
3396 ldv_final:
3397 {
3398#line 430
3399 ldv_check_final_state();
3400 }
3401#line 433
3402 return;
3403}
3404}
3405#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2877/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3406void ldv_blast_assert(void)
3407{
3408
3409 {
3410 ERROR: ;
3411#line 6
3412 goto ERROR;
3413}
3414}
3415#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2877/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3416extern int __VERIFIER_nondet_int(void) ;
3417#line 454 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2877/dscv_tempdir/dscv/ri/43_1a/drivers/input/joystick/warrior.c.p"
3418int ldv_spin = 0;
3419#line 458 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2877/dscv_tempdir/dscv/ri/43_1a/drivers/input/joystick/warrior.c.p"
3420void ldv_check_alloc_flags(gfp_t flags )