Showing error 131

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-media-video-msp3400.ko_safe.cil.out.i.pp.cil.c
Line in file: 10424
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

10394#line 1373
10395        goto switch_break;
10396      } else {
10397        switch_break: ;
10398      }
10399    }
10400  }
10401  while_break___0: /* CIL Label */ ;
10402  }
10403
10404  while_break: ;
10405  ldv_module_exit: 
10406  {
10407#line 1389
10408  exit_msp();
10409  }
10410  ldv_final: 
10411  {
10412#line 1392
10413  ldv_check_final_state();
10414  }
10415#line 1395
10416  return;
10417}
10418}
10419#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/media/video/msp3400.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/22/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast-assert.h"
10420void ldv_blast_assert(void) 
10421{ 
10422
10423  {
10424  ERROR: 
10425#line 6
10426  goto ERROR;
10427}
10428}
10429#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/media/video/msp3400.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/22/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast.h"
10430extern void *ldv_undefined_pointer(void) ;
10431#line 1332 "include/linux/usb.h"
10432struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags )  __attribute__((__ldv_model__)) ;
10433#line 1333
10434void usb_free_urb(struct urb *urb )  __attribute__((__ldv_model__)) ;
Show full sources
↑