Showing error 821

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

Source: 

3087  tmp___0 = __VERIFIER_nondet_int();
3088  }
3089#line 367
3090  if (tmp___0 != 0) {
3091#line 369
3092    goto ldv_18932;
3093  } else
3094#line 367
3095  if (ldv_s_max8688_driver_i2c_driver != 0) {
3096#line 369
3097    goto ldv_18932;
3098  } else {
3099#line 371
3100    goto ldv_18934;
3101  }
3102  ldv_18934: ;
3103  ldv_module_exit: ;
3104  {
3105#line 505
3106  ldv_check_final_state();
3107  }
3108#line 508
3109  return;
3110}
3111}
3112#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/10885/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3113void ldv_blast_assert(void) 
3114{ 
3115
3116  {
3117  ERROR: ;
3118#line 6
3119  goto ERROR;
3120}
3121}
3122#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/10885/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3123extern int __VERIFIER_nondet_int(void) ;
3124#line 529 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/10885/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/pmbus/max8688.c.p"
3125int ldv_spin  =    0;
3126#line 533 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/10885/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/pmbus/max8688.c.p"
3127void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑