4047 switch_default:
4048#line 343
4049 goto switch_break;
4050 } else {
4051 switch_break: ;
4052 }
4053 }
4054 }
4055 }
4056 while_break: ;
4057 }
4058 ldv_module_exit:
4059 {
4060#line 355
4061 tps65217_exit();
4062 }
4063 ldv_final:
4064 {
4065#line 358
4066 ldv_check_final_state();
4067 }
4068#line 361
4069 return;
4070}
4071}
4072#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/8232/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4073void ldv_blast_assert(void)
4074{
4075
4076 {
4077 ERROR:
4078#line 6
4079 goto ERROR;
4080}
4081}
4082#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/8232/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4083extern int __VERIFIER_nondet_int(void) ;
4084#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/8232/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4085int ldv_mutex = 1;
4086#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/8232/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4087int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )