4943 goto ldv_31314;
4944 } else
4945#line 269
4946 if (ldv_s_avmcs_driver_pcmcia_driver != 0) {
4947#line 271
4948 goto ldv_31314;
4949 } else {
4950#line 273
4951 goto ldv_31316;
4952 }
4953 ldv_31316: ;
4954 ldv_module_exit:
4955 {
4956#line 322
4957 avmcs_exit();
4958 }
4959 ldv_final:
4960 {
4961#line 325
4962 ldv_check_final_state();
4963 }
4964#line 328
4965 return;
4966}
4967}
4968#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4156/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4969void ldv_blast_assert(void)
4970{
4971
4972 {
4973 ERROR: ;
4974#line 6
4975 goto ERROR;
4976}
4977}
4978#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4156/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4979extern int __VERIFIER_nondet_int(void) ;
4980#line 349 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4156/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/avm_cs.c.p"
4981int ldv_spin = 0;
4982#line 353 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4156/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/avm_cs.c.p"
4983void ldv_check_alloc_flags(gfp_t flags )