3195 goto ldv_20790;
3196 } else
3197#line 315
3198 if (ldv_s_gunze_drv_serio_driver != 0) {
3199#line 317
3200 goto ldv_20790;
3201 } else {
3202#line 319
3203 goto ldv_20792;
3204 }
3205 ldv_20792: ;
3206 ldv_module_exit:
3207 {
3208#line 396
3209 gunze_exit();
3210 }
3211 ldv_final:
3212 {
3213#line 399
3214 ldv_check_final_state();
3215 }
3216#line 402
3217 return;
3218}
3219}
3220#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3106/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3221void ldv_blast_assert(void)
3222{
3223
3224 {
3225 ERROR: ;
3226#line 6
3227 goto ERROR;
3228}
3229}
3230#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3106/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3231extern int __VERIFIER_nondet_int(void) ;
3232#line 423 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3106/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/gunze.c.p"
3233int ldv_spin = 0;
3234#line 427 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3106/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/gunze.c.p"
3235void ldv_check_alloc_flags(gfp_t flags )