11228 switch_default:
11229#line 3318
11230 goto switch_break;
11231 } else {
11232 switch_break: ;
11233 }
11234 }
11235 }
11236 }
11237 while_break: ;
11238 }
11239 ldv_module_exit:
11240 {
11241#line 3351
11242 m2mtest_exit();
11243 }
11244 ldv_final:
11245 {
11246#line 3354
11247 ldv_check_final_state();
11248 }
11249#line 3357
11250 return;
11251}
11252}
11253#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/15010/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
11254void ldv_blast_assert(void)
11255{
11256
11257 {
11258 ERROR:
11259#line 6
11260 goto ERROR;
11261}
11262}
11263#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/15010/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
11264extern int __VERIFIER_nondet_int(void) ;
11265#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/15010/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
11266int ldv_mutex = 1;
11267#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/15010/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
11268int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )