3204 goto ldv_20792;
3205 } else
3206#line 353
3207 if (ldv_s_dynapro_drv_serio_driver != 0) {
3208#line 355
3209 goto ldv_20792;
3210 } else {
3211#line 357
3212 goto ldv_20794;
3213 }
3214 ldv_20794: ;
3215 ldv_module_exit:
3216 {
3217#line 470
3218 dynapro_exit();
3219 }
3220 ldv_final:
3221 {
3222#line 473
3223 ldv_check_final_state();
3224 }
3225#line 476
3226 return;
3227}
3228}
3229#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3101/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3230void ldv_blast_assert(void)
3231{
3232
3233 {
3234 ERROR: ;
3235#line 6
3236 goto ERROR;
3237}
3238}
3239#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3101/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3240extern int __VERIFIER_nondet_int(void) ;
3241#line 497 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3101/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/dynapro.c.p"
3242int ldv_spin = 0;
3243#line 501 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3101/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/dynapro.c.p"
3244void ldv_check_alloc_flags(gfp_t flags )