4540 {
4541#line 199
4542 usb_debug_process_read_urb(var_group2);
4543 }
4544#line 206
4545 goto switch_break;
4546 switch_default:
4547#line 207
4548 goto switch_break;
4549 } else {
4550 switch_break: ;
4551 }
4552 }
4553 }
4554 }
4555 while_break: ;
4556 }
4557 {
4558#line 216
4559 ldv_check_final_state();
4560 }
4561#line 219
4562 return;
4563}
4564}
4565#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7562/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4566void ldv_blast_assert(void)
4567{
4568
4569 {
4570 ERROR:
4571#line 6
4572 goto ERROR;
4573}
4574}
4575#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7562/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4576extern int __VERIFIER_nondet_int(void) ;
4577#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7562/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4578int ldv_mutex = 1;
4579#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7562/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4580int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )