4848 switch_default:
4849#line 324
4850 goto switch_break;
4851 } else {
4852 switch_break: ;
4853 }
4854 }
4855 }
4856 }
4857 while_break: ;
4858 }
4859 ldv_module_exit:
4860 {
4861#line 338
4862 cfag12864bfb_exit();
4863 }
4864 ldv_final:
4865 {
4866#line 341
4867 ldv_check_final_state();
4868 }
4869#line 344
4870 return;
4871}
4872}
4873#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16869/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4874void ldv_blast_assert(void)
4875{
4876
4877 {
4878 ERROR:
4879#line 6
4880 goto ERROR;
4881}
4882}
4883#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16869/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4884extern int __VERIFIER_nondet_int(void) ;
4885#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16869/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4886int ldv_mutex = 1;
4887#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16869/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4888int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )