Showing error 149

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

Source: 

13278#line 2598
13279        goto switch_break;
13280      } else {
13281        switch_break: ;
13282      }
13283    }
13284  }
13285  while_break___0: /* CIL Label */ ;
13286  }
13287
13288  while_break: ;
13289  ldv_module_exit: 
13290  {
13291#line 2626
13292  whiteheat_exit();
13293  }
13294  ldv_final: 
13295  {
13296#line 2629
13297  ldv_check_final_state();
13298  }
13299#line 2632
13300  return;
13301}
13302}
13303#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/whiteheat.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"
13304void ldv_blast_assert(void) 
13305{ 
13306
13307  {
13308  ERROR: 
13309#line 6
13310  goto ERROR;
13311}
13312}
13313#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/whiteheat.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"
13314extern void *ldv_undefined_pointer(void) ;
13315#line 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/whiteheat.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"
13316void ldv_assume_stop(void)  __attribute__((__ldv_model_inline__)) ;
13317#line 22
13318void ldv_assume_stop(void)  __attribute__((__ldv_model_inline__)) ;
Show full sources
↑