Showing error 689

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_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--usb--serial--metro-usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 7943
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

7913#line 875
7914        metrousb_tiocmset(var_group1, var_metrousb_tiocmset_8_p1, var_metrousb_tiocmset_8_p2);
7915        }
7916#line 882
7917        goto switch_break;
7918        switch_default: /* CIL Label */ 
7919#line 883
7920        goto switch_break;
7921      } else {
7922        switch_break: /* CIL Label */ ;
7923      }
7924      }
7925    }
7926  }
7927  while_break: /* CIL Label */ ;
7928  }
7929  ldv_module_exit: 
7930  {
7931#line 892
7932  ldv_check_final_state();
7933  }
7934#line 895
7935  return;
7936}
7937}
7938#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7543/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
7939void ldv_blast_assert(void) 
7940{ 
7941
7942  {
7943  ERROR: 
7944#line 6
7945  goto ERROR;
7946}
7947}
7948#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7543/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
7949extern int __VERIFIER_nondet_int(void) ;
7950#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7543/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7951int ldv_mutex  =    1;
7952#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7543/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7953int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock )
Show full sources
↑