Showing error 210

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-video-arkfb.ko-safe.cil.out.i.pp.cil.c
Line in file: 12158
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

12128#line 2402
12129        goto switch_break;
12130      } else {
12131        switch_break: ;
12132      }
12133    }
12134  }
12135  while_break___0: /* CIL Label */ ;
12136  }
12137
12138  while_break: ;
12139  ldv_module_exit: 
12140  {
12141#line 2431
12142  arkfb_cleanup();
12143  }
12144  ldv_final: 
12145  {
12146#line 2438
12147  ldv_check_final_state();
12148  }
12149#line 2441
12150  return;
12151}
12152}
12153#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/video/arkfb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast-assert.h"
12154void ldv_blast_assert(void) 
12155{ 
12156
12157  {
12158  ERROR: 
12159#line 6
12160  goto ERROR;
12161}
12162}
12163#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/video/arkfb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast.h"
12164extern void *ldv_undefined_pointer(void) ;
12165#line 1332 "include/linux/usb.h"
12166struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags )  __attribute__((__ldv_model__)) ;
12167#line 1333
12168void usb_free_urb(struct urb *urb )  __attribute__((__ldv_model__)) ;
Show full sources
↑