7355
7356 }
7357 }
7358 {
7359#line 360
7360 flags = _raw_write_lock_irqsave(& bp_lock);
7361#line 361
7362 __cil_tmp6 = & bp->list;
7363#line 361
7364 list_del(__cil_tmp6);
7365#line 362
7366 _raw_write_unlock_irqrestore(& bp_lock, flags);
7367 }
7368#line 363
7369 return;
7370}
7371}
7372#line 435
7373void ldv_check_final_state(void) ;
7374#line 441
7375extern void ldv_initialize(void) ;
7376#line 444
7377extern int nondet_int(void) ;
7378#line 447 "/anthill/stuff/tacas-comp/work/current--X--drivers/isdn/mISDN/mISDN_core.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/30/dscv_tempdir/dscv/ri/08_1/drivers/isdn/mISDN/core.c.p"
7379int LDV_IN_INTERRUPT ;
7380#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/isdn/mISDN/mISDN_core.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/30/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
7381void ldv_blast_assert(void)
7382{
7383
7384 {
7385 ERROR: ;
7386#line 6
7387 goto ERROR;
7388}
7389}
7390#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/isdn/mISDN/mISDN_core.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/30/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast.h"
7391extern int ldv_undefined_int(void) ;
7392#line 660 "/anthill/stuff/tacas-comp/work/current--X--drivers/isdn/mISDN/mISDN_core.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/30/dscv_tempdir/dscv/ri/08_1/drivers/isdn/mISDN/core.c.p"
7393int ldv_module_refcounter = 1;
7394#line 663 "/anthill/stuff/tacas-comp/work/current--X--drivers/isdn/mISDN/mISDN_core.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/30/dscv_tempdir/dscv/ri/08_1/drivers/isdn/mISDN/core.c.p"
7395void ldv_module_get(struct module *module )