3093 goto ldv_20787;
3094 } else
3095#line 300
3096 if (ldv_s_fujitsu_drv_serio_driver != 0) {
3097#line 302
3098 goto ldv_20787;
3099 } else {
3100#line 304
3101 goto ldv_20789;
3102 }
3103 ldv_20789: ;
3104 ldv_module_exit:
3105 {
3106#line 381
3107 fujitsu_exit();
3108 }
3109 ldv_final:
3110 {
3111#line 384
3112 ldv_check_final_state();
3113 }
3114#line 387
3115 return;
3116}
3117}
3118#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3105/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3119void ldv_blast_assert(void)
3120{
3121
3122 {
3123 ERROR: ;
3124#line 6
3125 goto ERROR;
3126}
3127}
3128#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3105/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3129extern int __VERIFIER_nondet_int(void) ;
3130#line 408 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3105/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/fujitsu_ts.c.p"
3131int ldv_spin = 0;
3132#line 412 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3105/dscv_tempdir/dscv/ri/43_1a/drivers/input/touchscreen/fujitsu_ts.c.p"
3133void ldv_check_alloc_flags(gfp_t flags )