14399 } else
14400# 3742 "/anthill/stuff/tacas-comp/work/current--X--drivers/atm/eni.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/atm/eni.c.p"
14401 if (ldv_s_ops_atmdev_ops != 0) {
14402# 3745 "/anthill/stuff/tacas-comp/work/current--X--drivers/atm/eni.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/atm/eni.c.p"
14403 goto ldv_40768;
14404 } else
14405# 3742 "/anthill/stuff/tacas-comp/work/current--X--drivers/atm/eni.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/atm/eni.c.p"
14406 if (ldv_s_eni_driver_pci_driver != 0) {
14407# 3745 "/anthill/stuff/tacas-comp/work/current--X--drivers/atm/eni.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/atm/eni.c.p"
14408 goto ldv_40768;
14409 } else {
14410# 3747 "/anthill/stuff/tacas-comp/work/current--X--drivers/atm/eni.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/atm/eni.c.p"
14411 goto ldv_40770;
14412 }
14413 ldv_40770: ;
14414 ldv_module_exit: ;
14415 ldv_final:
14416 {
14417# 5134 "/anthill/stuff/tacas-comp/work/current--X--drivers/atm/eni.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/atm/eni.c.p"
14418 ldv_check_final_state();
14419 }
14420# 5137 "/anthill/stuff/tacas-comp/work/current--X--drivers/atm/eni.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/atm/eni.c.p"
14421 return;
14422}
14423}
14424# 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/atm/eni.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
14425void ldv_blast_assert(void)
14426{
14427
14428 {
14429 ERROR: ;
14430# 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/atm/eni.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
14431 goto ERROR;
14432}
14433}
14434# 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/atm/eni.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast.h"
14435extern int ldv_undefined_int(void) ;
14436# 5154 "/anthill/stuff/tacas-comp/work/current--X--drivers/atm/eni.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/atm/eni.c.p"
14437int ldv_module_refcounter = 1;
14438# 5157 "/anthill/stuff/tacas-comp/work/current--X--drivers/atm/eni.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/atm/eni.c.p"
14439void ldv_module_get(struct module *module )