Showing error 1315

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

Source: 

3775    goto ldv_18232;
3776  } else
3777#line 720
3778  if (ldv_s_it8712f_wdt_fops_file_operations != 0) {
3779#line 722
3780    goto ldv_18232;
3781  } else {
3782#line 724
3783    goto ldv_18234;
3784  }
3785  ldv_18234: ;
3786  ldv_module_exit: 
3787  {
3788#line 968
3789  it8712f_wdt_exit();
3790  }
3791  ldv_final: 
3792  {
3793#line 971
3794  ldv_check_final_state();
3795  }
3796#line 974
3797  return;
3798}
3799}
3800#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3801void ldv_blast_assert(void) 
3802{ 
3803
3804  {
3805  ERROR: ;
3806#line 6
3807  goto ERROR;
3808}
3809}
3810#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3811extern int __VERIFIER_nondet_int(void) ;
3812#line 995 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3813int ldv_spin  =    0;
3814#line 999 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3815void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑