11510 kfree(__cil_tmp46);
11511 }
11512#line 1148
11513 return ((struct gigaset_driver *)0);
11514}
11515}
11516#line 1159 "/anthill/stuff/tacas-comp/work/current--X--drivers/isdn/gigaset/gigaset.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/20/dscv_tempdir/dscv/ri/08_1/drivers/isdn/gigaset/common.c.p"
11517void gigaset_blockdriver(struct gigaset_driver *drv )
11518{
11519
11520 {
11521#line 1161
11522 drv->blocked = 1;
11523#line 1162
11524 return;
11525}
11526}
11527#line 1208
11528void ldv_check_final_state(void) ;
11529#line 1214
11530extern void ldv_initialize(void) ;
11531#line 1217
11532extern int nondet_int(void) ;
11533#line 1220 "/anthill/stuff/tacas-comp/work/current--X--drivers/isdn/gigaset/gigaset.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/20/dscv_tempdir/dscv/ri/08_1/drivers/isdn/gigaset/common.c.p"
11534int LDV_IN_INTERRUPT ;
11535#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/isdn/gigaset/gigaset.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/20/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
11536void ldv_blast_assert(void)
11537{
11538
11539 {
11540 ERROR: ;
11541#line 6
11542 goto ERROR;
11543}
11544}
11545#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/isdn/gigaset/gigaset.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/20/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast.h"
11546extern int ldv_undefined_int(void) ;
11547#line 1321 "/anthill/stuff/tacas-comp/work/current--X--drivers/isdn/gigaset/gigaset.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/20/dscv_tempdir/dscv/ri/08_1/drivers/isdn/gigaset/common.c.p"
11548int ldv_module_refcounter = 1;
11549#line 1324 "/anthill/stuff/tacas-comp/work/current--X--drivers/isdn/gigaset/gigaset.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/20/dscv_tempdir/dscv/ri/08_1/drivers/isdn/gigaset/common.c.p"
11550void ldv_module_get(struct module *module )