Showing error 1333

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

Source: 

2621    goto ldv_21747;
2622  } else
2623#line 357
2624  if (ldv_s_matrox_w1_pci_driver_pci_driver != 0) {
2625#line 359
2626    goto ldv_21747;
2627  } else {
2628#line 361
2629    goto ldv_21749;
2630  }
2631  ldv_21749: ;
2632  ldv_module_exit: 
2633  {
2634#line 414
2635  matrox_w1_fini();
2636  }
2637  ldv_final: 
2638  {
2639#line 417
2640  ldv_check_final_state();
2641  }
2642#line 420
2643  return;
2644}
2645}
2646#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4895/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2647void ldv_blast_assert(void) 
2648{ 
2649
2650  {
2651  ERROR: ;
2652#line 6
2653  goto ERROR;
2654}
2655}
2656#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4895/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2657extern int __VERIFIER_nondet_int(void) ;
2658#line 441 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4895/dscv_tempdir/dscv/ri/43_1a/drivers/w1/masters/matrox_w1.c.p"
2659int ldv_spin  =    0;
2660#line 445 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4895/dscv_tempdir/dscv/ri/43_1a/drivers/w1/masters/matrox_w1.c.p"
2661void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑