3256 goto ldv_20802;
3257 } else
3258#line 301
3259 if (ldv_s_tsc_drv_serio_driver != 0) {
3260#line 303
3261 goto ldv_20802;
3262 } else {
3263#line 305
3264 goto ldv_20804;
3265 }
3266 ldv_20804: ;
3267 ldv_module_exit:
3268 {
3269#line 388
3270 tsc_exit();
3271 }
3272 ldv_final:
3273 {
3274#line 391
3275 ldv_check_final_state();
3276 }
3277#line 394
3278 return;
3279}
3280}
3281#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3126/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3282void ldv_blast_assert(void)
3283{
3284
3285 {
3286 ERROR: ;
3287#line 6
3288 goto ERROR;
3289}
3290}
3291#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3126/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3292extern int __VERIFIER_nondet_int(void) ;
3293#line 415 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3126/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/tsc40.c.p"
3294int ldv_spin = 0;
3295#line 419 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3126/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/tsc40.c.p"
3296void ldv_check_alloc_flags(gfp_t flags )