13278#line 2598
13279 goto switch_break;
13280 } else {
13281 switch_break: ;
13282 }
13283 }
13284 }
13285 while_break___0: ;
13286 }
13287
13288 while_break: ;
13289 ldv_module_exit:
13290 {
13291#line 2626
13292 whiteheat_exit();
13293 }
13294 ldv_final:
13295 {
13296#line 2629
13297 ldv_check_final_state();
13298 }
13299#line 2632
13300 return;
13301}
13302}
13303#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/whiteheat.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast-assert.h"
13304void ldv_blast_assert(void)
13305{
13306
13307 {
13308 ERROR:
13309#line 6
13310 goto ERROR;
13311}
13312}
13313#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/whiteheat.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast.h"
13314extern void *ldv_undefined_pointer(void) ;
13315#line 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/whiteheat.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/model0068.c"
13316void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
13317#line 22
13318void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;