15185 }
15186 while_break___0: ;
15187# 1485 "/anthill/stuff/tacas-comp/work/current--X--drivers/vhost/vhost_net.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/12/dscv_tempdir/dscv/ri/68_1/drivers/vhost/vhost.c.common.c"
15188 if (vq->error_ctx) {
15189 {
15190# 1485 "/anthill/stuff/tacas-comp/work/current--X--drivers/vhost/vhost_net.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/12/dscv_tempdir/dscv/ri/68_1/drivers/vhost/vhost.c.common.c"
15191 eventfd_signal(vq->error_ctx, 1);
15192 }
15193 } else {
15194
15195 }
15196# 1485 "/anthill/stuff/tacas-comp/work/current--X--drivers/vhost/vhost_net.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/12/dscv_tempdir/dscv/ri/68_1/drivers/vhost/vhost.c.common.c"
15197 goto while_break;
15198 }
15199 while_break___1: ;
15200 }
15201 while_break: ;
15202 } else {
15203
15204 }
15205 }
15206# 1488 "/anthill/stuff/tacas-comp/work/current--X--drivers/vhost/vhost_net.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/12/dscv_tempdir/dscv/ri/68_1/drivers/vhost/vhost.c.common.c"
15207 return;
15208}
15209}
15210# 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/vhost/vhost_net.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/12/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast-assert.h"
15211void ldv_blast_assert(void)
15212{
15213
15214 {
15215 ERROR:
15216# 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/vhost/vhost_net.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/12/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast-assert.h"
15217 goto ERROR;
15218}
15219}
15220# 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/vhost/vhost_net.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/12/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast.h"
15221extern void *ldv_undefined_pointer(void) ;
15222# 1332 "include/linux/usb.h"
15223struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags ) __attribute__((__ldv_model__)) ;
15224# 1333 "include/linux/usb.h"
15225void usb_free_urb(struct urb *urb ) __attribute__((__ldv_model__)) ;