Showing error 1317

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

Source: 

4142    goto ldv_18268;
4143  } else
4144#line 945
4145  if (ldv_s_pc87413_fops_file_operations != 0) {
4146#line 947
4147    goto ldv_18268;
4148  } else {
4149#line 949
4150    goto ldv_18270;
4151  }
4152  ldv_18270: ;
4153  ldv_module_exit: 
4154  {
4155#line 1275
4156  pc87413_exit();
4157  }
4158  ldv_final: 
4159  {
4160#line 1278
4161  ldv_check_final_state();
4162  }
4163#line 1281
4164  return;
4165}
4166}
4167#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17353/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4168void ldv_blast_assert(void) 
4169{ 
4170
4171  {
4172  ERROR: ;
4173#line 6
4174  goto ERROR;
4175}
4176}
4177#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17353/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4178extern int __VERIFIER_nondet_int(void) ;
4179#line 1302 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17353/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/pc87413_wdt.c.p"
4180int ldv_spin  =    0;
4181#line 1306 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17353/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/pc87413_wdt.c.p"
4182void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑