Showing error 1259

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--uio--uio_aec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 3580
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

3550    goto ldv_25009;
3551  } else
3552#line 305
3553  if (ldv_s_pci_driver_pci_driver != 0) {
3554#line 307
3555    goto ldv_25009;
3556  } else {
3557#line 309
3558    goto ldv_25011;
3559  }
3560  ldv_25011: ;
3561  ldv_module_exit: 
3562  {
3563#line 394
3564  aectc_exit();
3565  }
3566  ldv_final: 
3567  {
3568#line 397
3569  ldv_check_final_state();
3570  }
3571#line 400
3572  return;
3573}
3574}
3575#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11177/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3576void ldv_blast_assert(void) 
3577{ 
3578
3579  {
3580  ERROR: ;
3581#line 6
3582  goto ERROR;
3583}
3584}
3585#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11177/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3586extern int __VERIFIER_nondet_int(void) ;
3587#line 421 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11177/dscv_tempdir/dscv/ri/43_1a/drivers/uio/uio_aec.c.p"
3588int ldv_spin  =    0;
3589#line 425 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11177/dscv_tempdir/dscv/ri/43_1a/drivers/uio/uio_aec.c.p"
3590void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑