11915 goto ldv_35976;
11916 } else
11917# 3466 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/sis900.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/net/sis900.c.p"
11918 if (ldv_s_sis900_pci_driver_pci_driver != 0) {
11919# 3469 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/sis900.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/net/sis900.c.p"
11920 goto ldv_35976;
11921 } else {
11922# 3471 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/sis900.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/net/sis900.c.p"
11923 goto ldv_35978;
11924 }
11925 ldv_35978: ;
11926 ldv_module_exit:
11927 {
11928# 4647 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/sis900.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/net/sis900.c.p"
11929 sis900_cleanup_module();
11930 }
11931 ldv_final:
11932 {
11933# 4650 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/sis900.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/net/sis900.c.p"
11934 ldv_check_final_state();
11935 }
11936# 4653 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/sis900.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/net/sis900.c.p"
11937 return;
11938}
11939}
11940# 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/sis900.ko--X--bulklinux-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"
11941void ldv_blast_assert(void)
11942{
11943
11944 {
11945 ERROR: ;
11946# 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/sis900.ko--X--bulklinux-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"
11947 goto ERROR;
11948}
11949}
11950# 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/sis900.ko--X--bulklinux-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"
11951extern int ldv_undefined_int(void) ;
11952# 4670 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/sis900.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/net/sis900.c.p"
11953int ldv_module_refcounter = 1;
11954# 4673 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/sis900.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/net/sis900.c.p"
11955void ldv_module_get(struct module *module )