Showing error 209

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.c
Line in file: 20447
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

20417        if (vq->error_ctx) {
20418          {
20419#line 1485
20420          __cil_tmp27 = vq->error_ctx;
20421#line 1485
20422          eventfd_signal(__cil_tmp27, 1);
20423          }
20424        } else {
20425
20426        }
20427#line 1485
20428        goto while_break;
20429      }
20430      while_break___1: /* CIL Label */ ;
20431      }
20432
20433      while_break: ;
20434    } else {
20435
20436    }
20437  }
20438#line 1488
20439  return;
20440}
20441}
20442#line 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"
20443void ldv_blast_assert(void) 
20444{ 
20445
20446  {
20447  ERROR: 
20448#line 6
20449  goto ERROR;
20450}
20451}
20452#line 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"
20453extern void *ldv_undefined_pointer(void) ;
20454#line 1332 "include/linux/usb.h"
20455struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags )  __attribute__((__ldv_model__)) ;
20456#line 1333
20457void usb_free_urb(struct urb *urb )  __attribute__((__ldv_model__)) ;
Show full sources
↑