2079 switch_default:
2080#line 198
2081 goto switch_break;
2082 } else {
2083 switch_break: ;
2084 }
2085 }
2086 }
2087 }
2088 while_break: ;
2089 }
2090 ldv_module_exit:
2091 {
2092#line 210
2093 pci_stub_exit();
2094 }
2095 ldv_final:
2096 {
2097#line 213
2098 ldv_check_final_state();
2099 }
2100#line 216
2101 return;
2102}
2103}
2104#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17435/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2105void ldv_blast_assert(void)
2106{
2107
2108 {
2109 ERROR:
2110#line 6
2111 goto ERROR;
2112}
2113}
2114#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17435/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2115extern int __VERIFIER_nondet_int(void) ;
2116#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17435/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2117int ldv_mutex = 1;
2118#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17435/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2119int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )