Showing error 1293

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--usb--storage--ums-sddr09.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 12144
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

12114  tmp___0 = __VERIFIER_nondet_int();
12115  }
12116#line 1922
12117  if (tmp___0 != 0) {
12118#line 1924
12119    goto ldv_31488;
12120  } else
12121#line 1922
12122  if (ldv_s_sddr09_driver_usb_driver != 0) {
12123#line 1924
12124    goto ldv_31488;
12125  } else {
12126#line 1926
12127    goto ldv_31490;
12128  }
12129  ldv_31490: ;
12130  ldv_module_exit: ;
12131  {
12132#line 2002
12133  ldv_check_final_state();
12134  }
12135#line 2005
12136  return;
12137}
12138}
12139#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2022/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
12140void ldv_blast_assert(void) 
12141{ 
12142
12143  {
12144  ERROR: ;
12145#line 6
12146  goto ERROR;
12147}
12148}
12149#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2022/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
12150extern int __VERIFIER_nondet_int(void) ;
12151#line 2026 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2022/dscv_tempdir/dscv/ri/43_1a/drivers/usb/storage/sddr09.c.p"
12152int ldv_spin  =    0;
12153#line 2030 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2022/dscv_tempdir/dscv/ri/43_1a/drivers/usb/storage/sddr09.c.p"
12154void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑