3298 switch_default:
3299#line 289
3300 goto switch_break;
3301 } else {
3302 switch_break: ;
3303 }
3304 }
3305 }
3306 }
3307 while_break: ;
3308 }
3309 ldv_module_exit:
3310 {
3311#line 304
3312 pl_exit();
3313 }
3314 ldv_final:
3315 {
3316#line 307
3317 ldv_check_final_state();
3318 }
3319#line 310
3320 return;
3321}
3322}
3323#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/211/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3324void ldv_blast_assert(void)
3325{
3326
3327 {
3328 ERROR:
3329#line 6
3330 goto ERROR;
3331}
3332}
3333#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/211/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3334extern int __VERIFIER_nondet_int(void) ;
3335#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/211/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3336int ldv_mutex = 1;
3337#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/211/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3338int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )