4242 goto switch_break;
4243 switch_default:
4244#line 596
4245 goto switch_break;
4246 } else {
4247 switch_break: ;
4248 }
4249 }
4250 }
4251 }
4252 while_break: ;
4253 }
4254 {
4255#line 613
4256 driver_parport_cleanup_module();
4257 }
4258 ldv_final:
4259 {
4260#line 619
4261 ldv_check_final_state();
4262 }
4263#line 622
4264 return;
4265}
4266}
4267#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1445/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4268void ldv_blast_assert(void)
4269{
4270
4271 {
4272 ERROR:
4273#line 6
4274 goto ERROR;
4275}
4276}
4277#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1445/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4278extern int __VERIFIER_nondet_int(void) ;
4279#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1445/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4280int ldv_mutex = 1;
4281#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1445/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4282int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )