3093#line 257
3094 LDV_IN_INTERRUPT = 1;
3095 }
3096#line 263
3097 goto switch_break;
3098 switch_default:
3099#line 264
3100 goto switch_break;
3101 } else {
3102 switch_break: ;
3103 }
3104 }
3105 }
3106 }
3107 while_break: ;
3108 }
3109 ldv_module_exit:
3110 {
3111#line 273
3112 ldv_check_final_state();
3113 }
3114#line 276
3115 return;
3116}
3117}
3118#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3994/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3119void ldv_blast_assert(void)
3120{
3121
3122 {
3123 ERROR:
3124#line 6
3125 goto ERROR;
3126}
3127}
3128#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3994/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3129extern int __VERIFIER_nondet_int(void) ;
3130#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3994/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3131int ldv_mutex = 1;
3132#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3994/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3133int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )