6278 goto ldv_27863;
6279 } else
6280#line 787
6281 if (ldv_s_ipaq_device_usb_serial_driver != 0) {
6282#line 789
6283 goto ldv_27863;
6284 } else {
6285#line 791
6286 goto ldv_27865;
6287 }
6288 ldv_27865: ;
6289 ldv_module_exit:
6290 {
6291#line 876
6292 ipaq_exit();
6293 }
6294 ldv_final:
6295 {
6296#line 879
6297 ldv_check_final_state();
6298 }
6299#line 882
6300 return;
6301}
6302}
6303#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1808/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6304void ldv_blast_assert(void)
6305{
6306
6307 {
6308 ERROR: ;
6309#line 6
6310 goto ERROR;
6311}
6312}
6313#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1808/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6314extern int __VERIFIER_nondet_int(void) ;
6315#line 903 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1808/dscv_tempdir/dscv/ri/43_1a/drivers/usb/serial/ipaq.c.p"
6316int ldv_spin = 0;
6317#line 907 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1808/dscv_tempdir/dscv/ri/43_1a/drivers/usb/serial/ipaq.c.p"
6318void ldv_check_alloc_flags(gfp_t flags )