Showing error 1337

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

Source: 

1647#line 269
1648  tmp___1 = __VERIFIER_nondet_int();
1649  }
1650#line 269
1651  if (tmp___1 != 0) {
1652#line 270
1653    goto ldv_15214;
1654  } else {
1655#line 272
1656    goto ldv_15216;
1657  }
1658  ldv_15216: ;
1659  {
1660#line 333
1661  w1_f1d_exit();
1662  }
1663  ldv_final: 
1664  {
1665#line 336
1666  ldv_check_final_state();
1667  }
1668#line 339
1669  return;
1670}
1671}
1672#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4909/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1673void ldv_blast_assert(void) 
1674{ 
1675
1676  {
1677  ERROR: ;
1678#line 6
1679  goto ERROR;
1680}
1681}
1682#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4909/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1683extern int __VERIFIER_nondet_int(void) ;
1684#line 360 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4909/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2423.c.p"
1685int ldv_spin  =    0;
1686#line 364 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4909/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2423.c.p"
1687void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑