Showing error 750

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/32_7_cilled_unsafe_const_ok_linux-32_1-drivers--usb--image--microtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 9012
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

8982#line 1481
8983        mts_slave_configure(var_group3);
8984        }
8985#line 1491
8986        goto switch_break;
8987        switch_default: /* CIL Label */ 
8988#line 1492
8989        goto switch_break;
8990      } else {
8991        switch_break: /* CIL Label */ ;
8992      }
8993      }
8994    }
8995  }
8996  while_break: /* CIL Label */ ;
8997  }
8998  ldv_module_exit: 
8999  {
9000#line 1501
9001  ldv_check_final_state();
9002  }
9003#line 1504
9004  return;
9005}
9006}
9007#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7795/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
9008void ldv_blast_assert(void) 
9009{ 
9010
9011  {
9012  ERROR: 
9013#line 6
9014  goto ERROR;
9015}
9016}
9017#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7795/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
9018extern int __VERIFIER_nondet_int(void) ;
9019#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7795/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9020int ldv_mutex  =    1;
9021#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7795/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9022int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock )
Show full sources
↑