Showing error 1123

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

Source: 

6309    goto ldv_37722;
6310  } else
6311#line 385
6312  if (ldv_s_mcp2120_dongle_driver != 0) {
6313#line 387
6314    goto ldv_37722;
6315  } else {
6316#line 389
6317    goto ldv_37724;
6318  }
6319  ldv_37724: ;
6320  ldv_module_exit: 
6321  {
6322#line 523
6323  mcp2120_sir_cleanup();
6324  }
6325  ldv_final: 
6326  {
6327#line 531
6328  ldv_check_final_state();
6329  }
6330#line 534
6331  return;
6332}
6333}
6334#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12689/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6335void ldv_blast_assert(void) 
6336{ 
6337
6338  {
6339  ERROR: ;
6340#line 6
6341  goto ERROR;
6342}
6343}
6344#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12689/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6345extern int __VERIFIER_nondet_int(void) ;
6346#line 555 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12689/dscv_tempdir/dscv/ri/43_1a/drivers/net/irda/mcp2120-sir.c.p"
6347int ldv_spin  =    0;
6348#line 559 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12689/dscv_tempdir/dscv/ri/43_1a/drivers/net/irda/mcp2120-sir.c.p"
6349void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑