3156 switch_default:
3157#line 431
3158 goto switch_break;
3159 } else {
3160 switch_break: ;
3161 }
3162 }
3163 }
3164 }
3165 while_break: ;
3166 }
3167 ldv_module_exit:
3168 {
3169#line 443
3170 mac_hid_exit();
3171 }
3172 ldv_final:
3173 {
3174#line 446
3175 ldv_check_final_state();
3176 }
3177#line 449
3178 return;
3179}
3180}
3181#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16570/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3182void ldv_blast_assert(void)
3183{
3184
3185 {
3186 ERROR:
3187#line 6
3188 goto ERROR;
3189}
3190}
3191#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16570/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3192extern int __VERIFIER_nondet_int(void) ;
3193#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16570/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3194int ldv_mutex = 1;
3195#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16570/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3196int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )