3241 goto ldv_19779;
3242 } else
3243#line 239
3244 if (ldv_s_pl_driver_hid_driver != 0) {
3245#line 241
3246 goto ldv_19779;
3247 } else {
3248#line 243
3249 goto ldv_19781;
3250 }
3251 ldv_19781: ;
3252 ldv_module_exit:
3253 {
3254#line 318
3255 pl_exit();
3256 }
3257 ldv_final:
3258 {
3259#line 321
3260 ldv_check_final_state();
3261 }
3262#line 324
3263 return;
3264}
3265}
3266#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4842/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3267void ldv_blast_assert(void)
3268{
3269
3270 {
3271 ERROR: ;
3272#line 6
3273 goto ERROR;
3274}
3275}
3276#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4842/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3277extern int __VERIFIER_nondet_int(void) ;
3278#line 345 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4842/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-petalynx.c.p"
3279int ldv_spin = 0;
3280#line 349 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4842/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-petalynx.c.p"
3281void ldv_check_alloc_flags(gfp_t flags )