Showing error 818

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

Source: 

3285  tmp___0 = __VERIFIER_nondet_int();
3286  }
3287#line 330
3288  if (tmp___0 != 0) {
3289#line 332
3290    goto ldv_18806;
3291  } else
3292#line 330
3293  if (ldv_s_max1111_driver_spi_driver != 0) {
3294#line 332
3295    goto ldv_18806;
3296  } else {
3297#line 334
3298    goto ldv_18808;
3299  }
3300  ldv_18808: ;
3301  ldv_module_exit: ;
3302  {
3303#line 377
3304  ldv_check_final_state();
3305  }
3306#line 380
3307  return;
3308}
3309}
3310#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11085/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3311void ldv_blast_assert(void) 
3312{ 
3313
3314  {
3315  ERROR: ;
3316#line 6
3317  goto ERROR;
3318}
3319}
3320#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11085/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3321extern int __VERIFIER_nondet_int(void) ;
3322#line 401 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11085/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/max1111.c.p"
3323int ldv_spin  =    0;
3324#line 405 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11085/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/max1111.c.p"
3325void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑