4916#line 639
4917 bmp085_detect(var_group1, var_group2);
4918 }
4919#line 646
4920 goto switch_break;
4921 switch_default:
4922#line 647
4923 goto switch_break;
4924 } else {
4925 switch_break: ;
4926 }
4927 }
4928 }
4929 }
4930 while_break: ;
4931 }
4932 ldv_module_exit:
4933 {
4934#line 656
4935 ldv_check_final_state();
4936 }
4937#line 659
4938 return;
4939}
4940}
4941#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4869/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4942void ldv_blast_assert(void)
4943{
4944
4945 {
4946 ERROR:
4947#line 6
4948 goto ERROR;
4949}
4950}
4951#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4869/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4952extern int __VERIFIER_nondet_int(void) ;
4953#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4869/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4954int ldv_mutex = 1;
4955#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4869/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4956int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )