4253 switch_default:
4254#line 413
4255 goto switch_break;
4256 } else {
4257 switch_break: ;
4258 }
4259 }
4260 }
4261 }
4262 while_break: ;
4263 }
4264 ldv_module_exit:
4265 {
4266#line 425
4267 i2c_smbus_exit();
4268 }
4269 ldv_final:
4270 {
4271#line 428
4272 ldv_check_final_state();
4273 }
4274#line 431
4275 return;
4276}
4277}
4278#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/391/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4279void ldv_blast_assert(void)
4280{
4281
4282 {
4283 ERROR:
4284#line 6
4285 goto ERROR;
4286}
4287}
4288#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/391/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4289extern int __VERIFIER_nondet_int(void) ;
4290#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/391/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4291int ldv_mutex = 1;
4292#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/391/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4293int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )