3270 goto ldv_20814;
3271 } else
3272#line 386
3273 if (ldv_s_twidjoy_drv_serio_driver != 0) {
3274#line 388
3275 goto ldv_20814;
3276 } else {
3277#line 390
3278 goto ldv_20816;
3279 }
3280 ldv_20816: ;
3281 ldv_module_exit:
3282 {
3283#line 467
3284 twidjoy_exit();
3285 }
3286 ldv_final:
3287 {
3288#line 470
3289 ldv_check_final_state();
3290 }
3291#line 473
3292 return;
3293}
3294}
3295#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2875/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3296void ldv_blast_assert(void)
3297{
3298
3299 {
3300 ERROR: ;
3301#line 6
3302 goto ERROR;
3303}
3304}
3305#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2875/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3306extern int __VERIFIER_nondet_int(void) ;
3307#line 494 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2875/dscv_tempdir/dscv/ri/43_1a/drivers/input/joystick/twidjoy.c.p"
3308int ldv_spin = 0;
3309#line 498 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2875/dscv_tempdir/dscv/ri/43_1a/drivers/input/joystick/twidjoy.c.p"
3310void ldv_check_alloc_flags(gfp_t flags )