Showing error 175

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

Source: 

1609#line 248
1610    if (0) {
1611      switch_default: /* CIL Label */ 
1612#line 250
1613      goto switch_break;
1614    } else {
1615      switch_break: /* CIL Label */ ;
1616    }
1617    }
1618  }
1619  while_break: /* CIL Label */ ;
1620  }
1621  {
1622#line 265
1623  ks0108_exit();
1624  }
1625  ldv_final: 
1626  {
1627#line 268
1628  ldv_check_final_state();
1629  }
1630#line 271
1631  return;
1632}
1633}
1634#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16870/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1635void ldv_blast_assert(void) 
1636{ 
1637
1638  {
1639  ERROR: 
1640#line 6
1641  goto ERROR;
1642}
1643}
1644#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16870/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1645extern int __VERIFIER_nondet_int(void) ;
1646#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16870/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1647int ldv_mutex  =    1;
1648#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16870/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1649int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock )
Show full sources
↑