Showing error 200

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

Source: 

10909        switch_default: 
10910#line 1564
10911        goto switch_break;
10912      } else {
10913        switch_break: ;
10914      }
10915    }
10916  }
10917  while_break___0: /* CIL Label */ ;
10918  }
10919
10920  while_break: 
10921  {
10922#line 1579
10923  sm_module_exit();
10924  }
10925  ldv_final: 
10926  {
10927#line 1582
10928  ldv_check_final_state();
10929  }
10930#line 1585
10931  return;
10932}
10933}
10934#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/mtd/sm_ftl.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"
10935void ldv_blast_assert(void) 
10936{ 
10937
10938  {
10939  ERROR: 
10940#line 6
10941  goto ERROR;
10942}
10943}
10944#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/mtd/sm_ftl.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"
10945extern void *ldv_undefined_pointer(void) ;
10946#line 1332 "include/linux/usb.h"
10947struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags )  __attribute__((__ldv_model__)) ;
10948#line 1333
10949void usb_free_urb(struct urb *urb )  __attribute__((__ldv_model__)) ;
Show full sources
↑