2981 goto ldv_20792;
2982 } else
2983#line 354
2984 if (ldv_s_zhenhua_drv_serio_driver != 0) {
2985#line 356
2986 goto ldv_20792;
2987 } else {
2988#line 358
2989 goto ldv_20794;
2990 }
2991 ldv_20794: ;
2992 ldv_module_exit:
2993 {
2994#line 435
2995 zhenhua_exit();
2996 }
2997 ldv_final:
2998 {
2999#line 438
3000 ldv_check_final_state();
3001 }
3002#line 441
3003 return;
3004}
3005}
3006#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2879/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3007void ldv_blast_assert(void)
3008{
3009
3010 {
3011 ERROR: ;
3012#line 6
3013 goto ERROR;
3014}
3015}
3016#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2879/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3017extern int __VERIFIER_nondet_int(void) ;
3018#line 462 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2879/dscv_tempdir/dscv/ri/43_1a/drivers/input/joystick/zhenhua.c.p"
3019int ldv_spin = 0;
3020#line 466 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2879/dscv_tempdir/dscv/ri/43_1a/drivers/input/joystick/zhenhua.c.p"
3021void ldv_check_alloc_flags(gfp_t flags )