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-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.c
Line in file: 9993
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

 9963#line 642
 9964  __wake_up(__cil_tmp4, 1U, 1, __cil_tmp5);
 9965#line 644
 9966  __cil_tmp6 = priv->main_thread.task;
 9967#line 644
 9968  kthread_stop(__cil_tmp6);
 9969#line 647
 9970  btmrvl_debugfs_remove(hdev);
 9971#line 650
 9972  hci_unregister_dev(hdev);
 9973#line 652
 9974  hci_free_dev(hdev);
 9975#line 654
 9976  priv->btmrvl_dev.hcidev = (struct hci_dev *)0;
 9977#line 656
 9978  btmrvl_free_adapter(priv);
 9979#line 658
 9980  __cil_tmp7 = (void const   *)priv;
 9981#line 658
 9982  kfree(__cil_tmp7);
 9983  }
 9984#line 660
 9985  return (0);
 9986}
 9987}
 9988#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/bluetooth/btmrvl.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/17/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
 9989void ldv_blast_assert(void) 
 9990{ 
 9991
 9992  {
 9993  ERROR: ;
 9994#line 6
 9995  goto ERROR;
 9996}
 9997}
 9998#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/bluetooth/btmrvl.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/17/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast.h"
 9999extern int ldv_undefined_int(void) ;
10000#line 676 "/anthill/stuff/tacas-comp/work/current--X--drivers/bluetooth/btmrvl.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/17/dscv_tempdir/dscv/ri/08_1/drivers/bluetooth/btmrvl_main.c.p"
10001void ldv_check_final_state(void) ;
10002#line 679 "/anthill/stuff/tacas-comp/work/current--X--drivers/bluetooth/btmrvl.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/17/dscv_tempdir/dscv/ri/08_1/drivers/bluetooth/btmrvl_main.c.p"
10003int ldv_module_refcounter  =    1;
Show full sources