./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] Setting "ana.int.interval" to true
[Info] function simple_fill_buf uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]   "up":
[Info]     simple_io
[Info]     verify_not_halted
[Info]     test_halt
[Info]     halt_simple
[Info]     verify_halted
[Info]     test_halt
[Info]     halt_simple
[Info]     test_unaligned_bulk
[Info]     usbtest_ioctl
[Info]     main
[Info]     usbtest_ioctl
[Info]     main
[Info]     unlink1
[Info]     unlink_simple
[Info]     usbtest_ioctl
[Info]     main
[Info]     unlink_queued
[Info]     usbtest_ioctl
[Info]     main
[Info] function simple_check_buf uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     check_guard_bytes
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     buffer_offset
[Info]   "up":
[Info]     simple_io
[Info]     verify_not_halted
[Info]     test_halt
[Info]     halt_simple
[Info]     verify_halted
[Info]     test_halt
[Info]     halt_simple
[Info]     test_unaligned_bulk
[Info]     usbtest_ioctl
[Info]     main
[Info]     usbtest_ioctl
[Info]     main
[Info]     unlink1
[Info]     unlink_simple
[Info]     usbtest_ioctl
[Info]     main
[Info] function simple_io uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     wait_for_completion_timeout
[Info]     __VERIFIER_nondet_ulong
[Info]     msecs_to_jiffies
[Info]     __VERIFIER_nondet_ulong
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     ldv_usb_submit_urb_21
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     usb_submit_urb
[Info]     __VERIFIER_nondet_int
[Info]     usb_kill_urb
[Info]     init_completion
[Info]     __init_waitqueue_head
[Info]     simple_fill_buf
[Info]     simple_check_buf
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     check_guard_bytes
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     buffer_offset
[Info]   "up":
[Info]     verify_not_halted
[Info]     test_halt
[Info]     halt_simple
[Info]     usbtest_ioctl
[Info]     verify_halted
[Info]     test_halt
[Info]     halt_simple
[Info]     usbtest_ioctl
[Info]     test_unaligned_bulk
[Info]     usbtest_ioctl
[Info]     main
[Info]     usbtest_ioctl
[Info]     main
[Info] function alloc_sglist uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     sg_init_table
[Info]     kmalloc_array
[Info]     __kmalloc
[Info]     ldv_malloc
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     kzalloc
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     sg_set_buf
[Info]     ldv__builtin_expect
[Info]     __phys_addr
[Info]     __VERIFIER_nondet_ulong
[Info]     __virt_addr_valid
[Info]     __VERIFIER_nondet_bool
[Info]     sg_set_page
[Info]     sg_assign_page
[Info]     ldv__builtin_expect
[Info]     free_sglist
[Info]     kfree
[Info]     sg_page
[Info]     ldv__builtin_expect
[Info]     sg_virt
[Info]     lowmem_page_address
[Info]     sg_page
[Info]     ldv__builtin_expect
[Info]   "up":
[Info]     usbtest_ioctl
[Info]     main
[Info] function ctrl_complete uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     complete
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     ldv_usb_submit_urb_22
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     usb_submit_urb
[Info]     __VERIFIER_nondet_int
[Info]     usb_unlink_urb
[Info]     __VERIFIER_nondet_int
[Info]     spin_lock
[Info]     ldv_spin_lock
[Info]     ldv_spin_lock_1
[Info]     _raw_spin_lock
[Info]     spin_unlock
[Info]     ldv_spin_unlock
[Info]     ldv_spin_unlock_5
[Info]     _raw_spin_unlock
[Info]   "up":
[Info] function test_ctrl_queue uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __raw_spin_lock_init
[Info]     wait_for_completion
[Info]     kfree
[Info]     dev_err
[Info]     __VERIFIER_nondet_int
[Info]     ldv_usb_submit_urb_23
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     usb_submit_urb
[Info]     __VERIFIER_nondet_int
[Info]     spinlock_check
[Info]     spin_lock_irq
[Info]     ldv_spin_lock
[Info]     ldv_spin_lock_irq_4
[Info]     _raw_spin_lock_irq
[Info]     spin_unlock_irq
[Info]     ldv_spin_unlock
[Info]     ldv_spin_unlock_irq_7
[Info]     _raw_spin_unlock_irq
[Info]     init_completion
[Info]     __init_waitqueue_head
[Info]     kmalloc
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     ldv_kmalloc_12
[Info]     __kmalloc
[Info]     ldv_malloc
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     kcalloc
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     ldv_kcalloc_14
[Info]     kmalloc_array
[Info]     __kmalloc
[Info]     ldv_malloc
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     __create_pipe
[Info]     testdev_to_usbdev
[Info]     interface_to_usbdev
[Info]     simple_alloc_urb
[Info]     usbtest_alloc_urb
[Info]     ldv_usb_alloc_urb_19
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     usb_alloc_urb
[Info]     ldv_malloc
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     usb_free_urb
[Info]     ldv_usb_alloc_coherent_20
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     usb_alloc_coherent
[Info]     ldv_malloc
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     kmalloc
[Info]     ldv_check_alloc_flags
[Info]     ldv_error
[Info]     reach_error
[Info]     ldv_kmalloc_12
[Info]     __kmalloc
[Info]     ldv_malloc
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     usb_fill_bulk_urb
[Info]     simple_free_urb
[Info]     kfree
[Info]     usb_free_urb
[Info]     usb_free_coherent
[Info]     buffer_offset
[Info]   "up":
[Info]     usbtest_ioctl
[Info]     main
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6805:3-6805:85)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6805:3-6805:85)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6805:3-6805:85)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7171:3-7171:73)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7171:3-7171:73)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7171:3-7171:73)
[Info][Unsound] Unknown value in {&(alloc@sid:68)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6829:3-6829:54)
[Info][Unsound] Unknown value in {&(alloc@sid:68)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6866:7-6866:97)
[Info][Unsound] Unknown value in {&(alloc@sid:68)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6597:3-6597:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4008:3-4008:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6598:7-6598:62)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:12:1-12:249)
[Warning][Deadcode] Function 'atomic_set' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3615:1-3621:1)
[Warning][Deadcode] Function 'atomic_inc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3622:1-3628:1)
[Warning][Deadcode] Function 'atomic_dec' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3629:1-3635:1)
[Warning][Deadcode] Function 'atomic_dec_and_test' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3636:1-3644:1)
[Warning][Deadcode] Function 'spinlock_check' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3650:1-3655:1)
[Warning][Deadcode] Function 'ldv_spin_lock_1' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3656:1-3662:1)
[Warning][Deadcode] Function 'ldv_spin_lock_irq_4' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3664:1-3670:1)
[Warning][Deadcode] Function 'ldv_spin_unlock_5' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3672:1-3678:1)
[Warning][Deadcode] Function 'ldv_spin_unlock_irq_7' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3680:1-3686:1)
[Warning][Deadcode] Function 'init_completion' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3693:1-3701:1)
[Warning][Deadcode] Function '__kmalloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3710:1-3713:1)
[Warning][Deadcode] Function 'ldv_kmalloc_12' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3715:1-3722:1)
[Warning][Deadcode] Function 'kmalloc_array' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3724:1-3735:1)
[Warning][Deadcode] Function 'ldv_kcalloc_14' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3736:1-3743:1)
[Warning][Deadcode] Function 'ldv_malloc' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3756:1-3772:1)
[Warning][Deadcode] Function 'ldv_undef_int' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3790:1-3797:1)
[Warning][Deadcode] Function 'ldv_undef_ulong' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3798:1-3805:1)
[Warning][Deadcode] Function 'ldv_error' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3806:1-3812:1)
[Warning][Deadcode] Function 'ldv__builtin_expect' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3820:1-3825:1)
[Warning][Deadcode] Function 'ldv__builtin_trap' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3826:1-3832:1)
[Warning][Deadcode] Function 'lowmem_page_address' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3840:1-3845:1)
[Warning][Deadcode] Function 'sg_assign_page' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3846:1-3881:1)
[Warning][Deadcode] Function 'sg_set_page' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3882:1-3891:1)
[Warning][Deadcode] Function 'sg_page' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3892:1-3915:1)
[Warning][Deadcode] Function 'sg_set_buf' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3916:1-3941:1)
[Warning][Deadcode] Function 'sg_virt' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3942:1-3951:1)
[Warning][Deadcode] Function 'usb_endpoint_type' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3953:1-3958:1)
[Warning][Deadcode] Function 'usb_endpoint_dir_in' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3959:1-3964:1)
[Warning][Deadcode] Function 'usb_endpoint_maxp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3965:1-3970:1)
[Warning][Deadcode] Function 'dev_get_drvdata' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3973:1-3978:1)
[Warning][Deadcode] Function 'dev_set_drvdata' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3979:1-3985:1)
[Warning][Deadcode] Function 'usb_get_intfdata' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3989:1-3996:1)
[Warning][Deadcode] Function 'usb_set_intfdata' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3997:1-4003:1)
[Warning][Deadcode] Function 'usb_fill_bulk_urb' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4017:1-4031:1)
[Warning][Deadcode] Function '__create_pipe' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4067:1-4072:1)
[Warning][Deadcode] Function 'testdev_to_usbdev' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4074:1-4081:1)
[Warning][Deadcode] Function 'get_endpoints' is uncalled: 62 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4082:1-4205:1)
[Warning][Deadcode] Function 'simple_callback' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4206:1-4212:1)
[Warning][Deadcode] Function 'usbtest_alloc_urb' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4213:1-4254:1)
[Warning][Deadcode] Function 'simple_alloc_urb' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4255:1-4262:1)
[Warning][Deadcode] Function 'simple_fill_buf' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4265:1-4297:1)
[Warning][Deadcode] Function 'buffer_offset' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4298:1-4303:1)
[Warning][Deadcode] Function 'check_guard_bytes' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4304:1-4332:1)
[Warning][Deadcode] Function 'simple_check_buf' is uncalled: 26 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4333:1-4382:1)
[Warning][Deadcode] Function 'simple_free_urb' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4383:1-4399:1)
[Warning][Deadcode] Function 'simple_io' is uncalled: 38 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4400:1-4473:1)
[Warning][Deadcode] Function 'free_sglist' is uncalled: 14 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4474:1-4504:1)
[Warning][Deadcode] Function 'alloc_sglist' is uncalled: 38 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4505:1-4575:1)
[Warning][Deadcode] Function 'perform_sglist' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4576:1-4616:1)
[Warning][Deadcode] Function 'get_altsetting' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4618:1-4641:1)
[Warning][Deadcode] Function 'set_altsetting' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4642:1-4658:1)
[Warning][Deadcode] Function 'is_good_config' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4659:1-4702:1)
[Warning][Deadcode] Function 'is_good_ext' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4703:1-4722:1)
[Warning][Deadcode] Function 'is_good_ss_cap' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4723:1-4745:1)
[Warning][Deadcode] Function 'is_good_con_id' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4746:1-4763:1)
[Warning][Deadcode] Function 'ch9_postconfig' is uncalled: 134 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:4764:1-5014:1)
[Warning][Deadcode] Function 'ctrl_complete' is uncalled: 56 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5015:1-5118:1)
[Warning][Deadcode] Function 'test_ctrl_queue' is uncalled: 172 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5119:1-5356:1)
[Warning][Deadcode] Function 'unlink1_callback' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5357:1-5373:1)
[Warning][Deadcode] Function 'unlink1' is uncalled: 45 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5374:1-5451:1)
[Warning][Deadcode] Function 'unlink_simple' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5452:1-5464:1)
[Warning][Deadcode] Function 'unlink_queued_callback' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5465:1-5496:1)
[Warning][Deadcode] Function 'unlink_queued' is uncalled: 63 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5497:1-5608:1)
[Warning][Deadcode] Function 'verify_not_halted' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5609:1-5634:1)
[Warning][Deadcode] Function 'verify_halted' is uncalled: 14 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5635:1-5665:1)
[Warning][Deadcode] Function 'test_halt' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5666:1-5711:1)
[Warning][Deadcode] Function 'halt_simple' is uncalled: 20 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5712:1-5752:1)
[Warning][Deadcode] Function 'ctrl_out' is uncalled: 57 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5753:1-5865:1)
[Warning][Deadcode] Function 'iso_callback' is uncalled: 31 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5866:1-5923:1)
[Warning][Deadcode] Function 'iso_alloc_urb' is uncalled: 37 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5924:1-5987:1)
[Warning][Deadcode] Function 'test_iso_queue' is uncalled: 68 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:5988:1-6108:1)
[Warning][Deadcode] Function 'test_unaligned_bulk' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6109:1-6128:1)
[Warning][Deadcode] Function 'usbtest_ioctl' is uncalled: 271 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6129:1-6574:1)
[Warning][Deadcode] Function 'usbtest_suspend' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6694:1-6699:1)
[Warning][Deadcode] Function 'usbtest_resume' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6700:1-6705:1)
[Warning][Deadcode] Function 'usbtest_disconnect' is uncalled: 14 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6706:1-6730:1)
[Warning][Deadcode] Function 'spin_lock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6982:1-6989:1)
[Warning][Deadcode] Function 'spin_lock_irq' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6990:1-6997:1)
[Warning][Deadcode] Function 'spin_unlock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6998:1-7005:1)
[Warning][Deadcode] Function 'spin_unlock_irq' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7006:1-7013:1)
[Warning][Deadcode] Function 'kmalloc' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7014:1-7021:1)
[Warning][Deadcode] Function 'kcalloc' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7023:1-7030:1)
[Warning][Deadcode] Function 'kzalloc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7032:1-7038:1)
[Warning][Deadcode] Function 'ldv_usb_alloc_urb_19' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7039:1-7047:1)
[Warning][Deadcode] Function 'ldv_usb_alloc_coherent_20' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7048:1-7056:1)
[Warning][Deadcode] Function 'ldv_usb_submit_urb_21' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7057:1-7065:1)
[Warning][Deadcode] Function 'ldv_usb_submit_urb_22' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7066:1-7074:1)
[Warning][Deadcode] Function 'ldv_usb_submit_urb_23' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7075:1-7083:1)
[Warning][Deadcode] Function 'ldv_usb_submit_urb_24' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7084:1-7092:1)
[Warning][Deadcode] Function 'ldv_usb_submit_urb_25' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7093:1-7101:1)
[Warning][Deadcode] Function 'ldv_usb_alloc_coherent_26' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7102:1-7110:1)
[Warning][Deadcode] Function 'ldv_usb_alloc_urb_27' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7111:1-7119:1)
[Warning][Deadcode] Function 'ldv_usb_submit_urb_28' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7120:1-7128:1)
[Warning][Deadcode] Function 'ldv_usb_submit_urb_29' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7129:1-7137:1)
[Warning][Deadcode] Function 'ldv_usb_alloc_urb_30' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7138:1-7146:1)
[Warning][Deadcode] Function 'ldv_usb_alloc_coherent_31' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7147:1-7155:1)
[Warning][Deadcode] Function 'ldv_usb_submit_urb_32' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7156:1-7164:1)
[Warning][Deadcode] Function 'ldv_check_alloc_flags' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7189:1-7198:1)
[Warning][Deadcode] Function 'ldv_check_alloc_flags_and_return_some_page' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7200:1-7211:1)
[Warning][Deadcode] Function 'ldv_check_alloc_nonatomic' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7212:1-7221:1)
[Warning][Deadcode] Function 'ldv_spin_lock' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7222:1-7228:1)
[Warning][Deadcode] Function 'ldv_spin_unlock' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7229:1-7235:1)
[Warning][Deadcode] Function 'ldv_spin_trylock' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7236:1-7248:1)
[Warning][Deadcode] Function '__dynamic_dev_dbg' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7250:1-7252:1)
[Warning][Deadcode] Function '__dynamic_pr_debug' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7254:1-7256:1)
[Warning][Deadcode] Function '__init_waitqueue_head' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7257:1-7259:1)
[Warning][Deadcode] Function '__mutex_init' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7260:1-7262:1)
[Warning][Deadcode] Function '__phys_addr' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7264:1-7266:1)
[Warning][Deadcode] Function '__raw_spin_lock_init' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7267:1-7269:1)
[Warning][Deadcode] Function '__virt_addr_valid' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7271:1-7273:1)
[Warning][Deadcode] Function '_dev_info' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7275:1-7277:1)
[Warning][Deadcode] Function '_raw_spin_lock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7278:1-7280:1)
[Warning][Deadcode] Function '_raw_spin_lock_irq' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7281:1-7283:1)
[Warning][Deadcode] Function '_raw_spin_unlock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7284:1-7286:1)
[Warning][Deadcode] Function '_raw_spin_unlock_irq' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7287:1-7289:1)
[Warning][Deadcode] Function 'complete' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7290:1-7292:1)
[Warning][Deadcode] Function 'completion_done' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7294:1-7296:1)
[Warning][Deadcode] Function 'dev_err' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7298:1-7300:1)
[Warning][Deadcode] Function 'dev_warn' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7302:1-7304:1)
[Warning][Deadcode] Function 'do_gettimeofday' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7305:1-7307:1)
[Warning][Deadcode] Function 'kmem_cache_alloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7308:1-7310:1)
[Warning][Deadcode] Function 'ldv_reset_resume_1' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7318:1-7320:1)
[Warning][Deadcode] Function 'ldv_some_page' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7321:1-7323:1)
[Warning][Deadcode] Function 'msecs_to_jiffies' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7325:1-7327:1)
[Warning][Deadcode] Function 'msleep' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7328:1-7330:1)
[Warning][Deadcode] Function 'mutex_lock_interruptible_nested' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7332:1-7334:1)
[Warning][Deadcode] Function 'mutex_unlock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7335:1-7337:1)
[Warning][Deadcode] Function 'sg_init_table' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7338:1-7340:1)
[Warning][Deadcode] Function 'usb_alloc_coherent' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7341:1-7343:1)
[Warning][Deadcode] Function 'usb_alloc_urb' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7344:1-7346:1)
[Warning][Deadcode] Function 'usb_clear_halt' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7348:1-7350:1)
[Warning][Deadcode] Function 'usb_control_msg' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7352:1-7354:1)
[Warning][Deadcode] Function 'usb_free_coherent' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7358:1-7360:1)
[Warning][Deadcode] Function 'usb_free_urb' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7361:1-7363:1)
[Warning][Deadcode] Function 'usb_get_descriptor' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7365:1-7367:1)
[Warning][Deadcode] Function 'usb_get_status' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7369:1-7371:1)
[Warning][Deadcode] Function 'usb_kill_urb' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7372:1-7374:1)
[Warning][Deadcode] Function 'usb_set_interface' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7380:1-7382:1)
[Warning][Deadcode] Function 'usb_sg_init' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7384:1-7386:1)
[Warning][Deadcode] Function 'usb_sg_wait' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7387:1-7389:1)
[Warning][Deadcode] Function 'usb_speed_string' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7390:1-7392:1)
[Warning][Deadcode] Function 'usb_submit_urb' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7394:1-7396:1)
[Warning][Deadcode] Function 'usb_unlink_urb' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7398:1-7400:1)
[Warning][Deadcode] Function 'wait_for_completion' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7401:1-7403:1)
[Warning][Deadcode] Function 'wait_for_completion_timeout' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7405:1-7407:1)
[Warning][Deadcode] Function 'kfree' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:7409:1-7411:1)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 6868..6869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6868-6869)
  on lines 6877..6879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6877-6879)
  on lines 6883..6885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6883-6885)
  on lines 6891..6893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6891-6893)
  on lines 6901..6903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6901-6903)
  on lines 6911..6912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6911-6912)
  on lines 6916..6917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6916-6917)
  on lines 6923..6925 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6923-6925)
[Warning][Deadcode] Function 'usbtest_init' has dead code:
  on lines 6791..6799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6791-6799)
[Warning][Deadcode] Function 'usbtest_probe' has dead code:
  on lines 6603..6604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6603-6604)
  on line 6607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6607-6607)
  on lines 6611..6614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6611-6614)
  on lines 6617..6625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6617-6625)
  on lines 6628..6636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6628-6636)
  on lines 6639..6642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6639-6642)
  on lines 6646..6649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6646-6649)
  on lines 6651..6653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6651-6653)
  on lines 6657..6659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6657-6659)
  on lines 6662..6664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6662-6664)
  on lines 6668..6669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6668-6669)
  on lines 6672..6673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6672-6673)
  on lines 6676..6677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6676-6677)
  on lines 6680..6681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6680-6681)
  on lines 6685..6688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6685-6688)
  on line 6691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6691-6691)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 104
  dead: 1696 (1611 in uncalled functions)
  total lines: 1800
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6865:9-6865:34)
[Warning][Deadcode][CWE-570] condition 'ldv_retval_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6867:11-6867:28)
[Warning][Deadcode][CWE-570] condition 'ldv_state_variable_1 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6876:9-6876:54)
[Warning][Deadcode][CWE-570] condition 'ldv_state_variable_1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6882:9-6882:54)
[Warning][Deadcode][CWE-570] condition 'ldv_state_variable_1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6890:9-6890:34)
[Warning][Deadcode][CWE-570] condition 'ldv_state_variable_1 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6900:9-6900:34)
[Warning][Deadcode][CWE-570] condition 'ldv_state_variable_1 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6910:9-6910:34)
[Warning][Deadcode][CWE-570] condition 'ldv_state_variable_1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6915:9-6915:34)
[Warning][Deadcode][CWE-570] condition 'ldv_state_variable_1 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6922:9-6922:34)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_0 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6939:7-6939:32)
[Warning][Deadcode][CWE-570] condition '(unsigned int )vendor != 0U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6790:7-6790:34)
[Warning][Deadcode][CWE-571] condition 'ref_cnt == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6943:9-6943:50)
[Warning][Deadcode][CWE-571] condition '(unsigned int )((unsigned short )id->match_flags) == 0U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6598:7-6598:62)
[Warning][Deadcode][CWE-571] condition '(unsigned int )vendor == 0U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:6599:9-6599:87)
[Warning][Deadcode][CWE-570] condition '! cond' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--misc--usbtest.ko-entry_point.cil.out.i:3754:6-3754:11)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
