3183 goto ldv_20793;
3184 } else
3185#line 369
3186 if (ldv_s_touchit213_drv_serio_driver != 0) {
3187#line 371
3188 goto ldv_20793;
3189 } else {
3190#line 373
3191 goto ldv_20795;
3192 }
3193 ldv_20795: ;
3194 ldv_module_exit:
3195 {
3196#line 474
3197 touchit213_exit();
3198 }
3199 ldv_final:
3200 {
3201#line 477
3202 ldv_check_final_state();
3203 }
3204#line 480
3205 return;
3206}
3207}
3208#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3120/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3209void ldv_blast_assert(void)
3210{
3211
3212 {
3213 ERROR: ;
3214#line 6
3215 goto ERROR;
3216}
3217}
3218#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3120/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3219extern int __VERIFIER_nondet_int(void) ;
3220#line 501 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3120/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/touchit213.c.p"
3221int ldv_spin = 0;
3222#line 505 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3120/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/touchit213.c.p"
3223void ldv_check_alloc_flags(gfp_t flags )