4427 goto switch_break;
4428 switch_default:
4429#line 375
4430 goto switch_break;
4431 } else {
4432 switch_break: ;
4433 }
4434 }
4435 }
4436 }
4437 while_break: ;
4438 }
4439 {
4440#line 393
4441 i2c_stub_exit();
4442 }
4443 ldv_final:
4444 {
4445#line 396
4446 ldv_check_final_state();
4447 }
4448#line 399
4449 return;
4450}
4451}
4452#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4453void ldv_blast_assert(void)
4454{
4455
4456 {
4457 ERROR:
4458#line 6
4459 goto ERROR;
4460}
4461}
4462#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4463extern int __VERIFIER_nondet_int(void) ;
4464#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4465int ldv_mutex = 1;
4466#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4467int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )