Showing error 1326

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

Source: 

5188    goto ldv_25294;
5189  } else
5190#line 1047
5191  if (ldv_s_wdtpci_driver_pci_driver != 0) {
5192#line 1051
5193    goto ldv_25294;
5194  } else {
5195#line 1053
5196    goto ldv_25296;
5197  }
5198  ldv_25296: ;
5199  ldv_module_exit: 
5200  {
5201#line 1346
5202  wdtpci_cleanup();
5203  }
5204  ldv_final: 
5205  {
5206#line 1349
5207  ldv_check_final_state();
5208  }
5209#line 1352
5210  return;
5211}
5212}
5213#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5214void ldv_blast_assert(void) 
5215{ 
5216
5217  {
5218  ERROR: ;
5219#line 6
5220  goto ERROR;
5221}
5222}
5223#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5224extern int __VERIFIER_nondet_int(void) ;
5225#line 1373 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5226int ldv_spin  =    0;
5227#line 1377 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5228void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑