Showing error 1207

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--scsi--pcmcia--sym53c500_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 9128
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

9098    goto ldv_31999;
9099  } else
9100#line 1869
9101  if (ldv_s_sym53c500_cs_driver_pcmcia_driver != 0) {
9102#line 1871
9103    goto ldv_31999;
9104  } else {
9105#line 1873
9106    goto ldv_32001;
9107  }
9108  ldv_32001: ;
9109  ldv_module_exit: 
9110  {
9111#line 2862
9112  exit_sym53c500_cs();
9113  }
9114  ldv_final: 
9115  {
9116#line 2865
9117  ldv_check_final_state();
9118  }
9119#line 2868
9120  return;
9121}
9122}
9123#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3635/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
9124void ldv_blast_assert(void) 
9125{ 
9126
9127  {
9128  ERROR: ;
9129#line 6
9130  goto ERROR;
9131}
9132}
9133#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3635/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
9134extern int __VERIFIER_nondet_int(void) ;
9135#line 2889 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3635/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/pcmcia/sym53c500_cs.c.p"
9136int ldv_spin  =    0;
9137#line 2893 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3635/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/pcmcia/sym53c500_cs.c.p"
9138void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑