Showing error 1338

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

Source: 

2172#line 508
2173  tmp___1 = __VERIFIER_nondet_int();
2174  }
2175#line 508
2176  if (tmp___1 != 0) {
2177#line 509
2178    goto ldv_15249;
2179  } else {
2180#line 511
2181    goto ldv_15251;
2182  }
2183  ldv_15251: ;
2184  {
2185#line 669
2186  w1_f2d_fini();
2187  }
2188  ldv_final: 
2189  {
2190#line 672
2191  ldv_check_final_state();
2192  }
2193#line 675
2194  return;
2195}
2196}
2197#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4910/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2198void ldv_blast_assert(void) 
2199{ 
2200
2201  {
2202  ERROR: ;
2203#line 6
2204  goto ERROR;
2205}
2206}
2207#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4910/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2208extern int __VERIFIER_nondet_int(void) ;
2209#line 696 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4910/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2431.c.p"
2210int ldv_spin  =    0;
2211#line 700 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4910/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2431.c.p"
2212void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑