4177 goto switch_break;
4178 switch_default:
4179#line 650
4180 goto switch_break;
4181 } else {
4182 switch_break: ;
4183 }
4184 }
4185 }
4186 }
4187 while_break: ;
4188 }
4189 {
4190#line 676
4191 driver_8255_cleanup_module();
4192 }
4193 ldv_final:
4194 {
4195#line 679
4196 ldv_check_final_state();
4197 }
4198#line 682
4199 return;
4200}
4201}
4202#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1407/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4203void ldv_blast_assert(void)
4204{
4205
4206 {
4207 ERROR:
4208#line 6
4209 goto ERROR;
4210}
4211}
4212#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1407/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4213extern int __VERIFIER_nondet_int(void) ;
4214#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1407/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4215int ldv_mutex = 1;
4216#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1407/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4217int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )