3114 goto ldv_20790;
3115 } else
3116#line 337
3117 if (ldv_s_stinger_drv_serio_driver != 0) {
3118#line 339
3119 goto ldv_20790;
3120 } else {
3121#line 341
3122 goto ldv_20792;
3123 }
3124 ldv_20792: ;
3125 ldv_module_exit:
3126 {
3127#line 418
3128 stinger_exit();
3129 }
3130 ldv_final:
3131 {
3132#line 421
3133 ldv_check_final_state();
3134 }
3135#line 424
3136 return;
3137}
3138}
3139#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2872/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3140void ldv_blast_assert(void)
3141{
3142
3143 {
3144 ERROR: ;
3145#line 6
3146 goto ERROR;
3147}
3148}
3149#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2872/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3150extern int __VERIFIER_nondet_int(void) ;
3151#line 445 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2872/dscv_tempdir/dscv/ri/43_1a/drivers/input/joystick/stinger.c.p"
3152int ldv_spin = 0;
3153#line 449 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2872/dscv_tempdir/dscv/ri/43_1a/drivers/input/joystick/stinger.c.p"
3154void ldv_check_alloc_flags(gfp_t flags )