Showing error 202

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-net-usb-catc.ko-unsafe.cil.out.i.pp.cil.c
Line in file: 11648
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

11618#line 1852
11619        goto switch_break;
11620      } else {
11621        switch_break: ;
11622      }
11623    }
11624  }
11625  while_break___0: /* CIL Label */ ;
11626  }
11627
11628  while_break: ;
11629  ldv_module_exit: 
11630  {
11631#line 1892
11632  catc_exit();
11633  }
11634  ldv_final: 
11635  {
11636#line 1895
11637  ldv_check_final_state();
11638  }
11639#line 1898
11640  return;
11641}
11642}
11643#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/usb/catc.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"
11644void ldv_blast_assert(void) 
11645{ 
11646
11647  {
11648  ERROR: 
11649#line 6
11650  goto ERROR;
11651}
11652}
11653#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/usb/catc.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"
11654extern void *ldv_undefined_pointer(void) ;
11655#line 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/usb/catc.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/model0068.c"
11656void ldv_assume_stop(void)  __attribute__((__ldv_model_inline__)) ;
11657#line 22
11658void ldv_assume_stop(void)  __attribute__((__ldv_model_inline__)) ;
Show full sources
↑