./goblint --conf conf/svcomp.json --set ana.malloc.unique_address_count 1 --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-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.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] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] Setting "ana.int.interval" to true
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Unknown] lval (& ring)->tr_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6345:11-6345:34)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7616:3-7617:32)
[Info][Unsound] Unknown value in {&tx_ring.tr_lock.ldv_5961.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7616:3-7617:32)
[Warning][Unknown] lval (& ring)->tr_lock.ldv_5961.rlock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8216:3-8216:9)
[Info][Unsound] Unknown value in {&rx_ring.tr_lock.ldv_5961.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7616:3-7617:32)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7660:3-7660:44)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7660:3-7660:44)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7660:3-7660:44)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7835:3-7835:28)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7835:3-7835:28)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7835:3-7835:28)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7560:7-7560:27)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7564:7-7564:46)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7564:7-7564:46)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7565:5-7566:40)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7565:5-7566:40)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7570:3-7570:23)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7571:3-7571:46)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7544:3-7544:23)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7538:3-7538:44)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7538:3-7538:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7539:3-7539:40)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7576:3-7576:56)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7489:7-7489:42)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7287:5-7287:37)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7494:3-7494:21)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7459:3-7459:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7460:3-7463:78)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6934:3-6934:61)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6945:3-6945:53)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6891:3-6891:52)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6462:3-6462:14)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6463:3-6463:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6464:3-6464:14)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6465:3-6465:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6466:3-6466:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6467:3-6467:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6468:3-6468:13)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6469:3-6469:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6470:3-6470:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6471:3-6471:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6472:3-6472:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6473:3-6473:18)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6474:11-6474:38)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6894:3-6894:55)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6895:3-6895:51)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6895:3-6895:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6345:11-6345:34)
[Warning][Unknown] lval (& qdata)->cmd_hash_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6345:11-6345:34)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6896:3-6896:42)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6903:5-6903:32)
[Warning][Unknown] lval (& tcmd)->hash_list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8291:3-8291:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6916:3-6916:56)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6916:3-6916:56)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6351:3-6351:61)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6351:3-6351:61)
[Warning][Unknown] lval (& qdata)->cmd_hash_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6351:3-6351:61)
[Warning][Unknown] lval (& qdata)->cmd_hash_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8239:3-8239:9)
[Warning][Unknown] lval (& lock)->ldv_5961.rlock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8239:3-8239:9)
[Warning][Unknown] lval (& qdata)->cmd_hash_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6352:3-6352:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6954:5-6954:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6870:3-6870:51)
[Warning][Imprecise][Call] Function pointer *((shost->hostt)->eh_abort_handler) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6870:3-6870:51)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6870:3-6870:51)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6872:5-6872:72)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6875:3-6875:60)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6876:3-6876:37)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6876:3-6876:37)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6610:3-6610:44)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6611:3-6611:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6612:3-6612:48)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6612:3-6612:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6613:3-6613:30)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6613:3-6613:30)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6600:3-6600:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6600:3-6600:31)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6600:3-6600:31)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:22:136-22:139)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8259:10-8259:33)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8259:10-8259:33)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6601:3-6601:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6614:4-6614:22)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6615:3-6615:34)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6615:3-6615:34)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6768:3-6768:70)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6768:3-6768:70)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6769:11-6769:24)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6769:11-6769:24)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6616:3-6616:34)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6616:3-6616:34)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6568:3-6568:26)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6568:3-6568:26)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6569:3-6569:20)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6569:3-6569:20)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6570:3-6570:48)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6570:3-6570:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6571:3-6571:52)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6571:3-6571:52)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8284:3-8284:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6572:3-6572:38)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6572:3-6572:38)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6572:3-6572:38)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6345:11-6345:34)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6573:3-6573:38)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6573:3-6573:38)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:44:170-44:173)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8236:10-8236:35)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8236:10-8236:35)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6574:3-6574:27)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6574:3-6574:27)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8200:3-8200:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6575:3-6575:47)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6575:3-6575:47)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6575:3-6575:47)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6351:3-6351:61)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8239:3-8239:9)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6352:3-6352:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6576:3-6576:56)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6576:3-6576:56)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6576:3-6576:56)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8225:3-8225:9)
[Warning][Unknown] lval (& shost)->shost_gendev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8225:3-8225:9)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6577:3-6577:9)
[Warning][Unknown] lval (& tcmd)->work points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6617:3-6617:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6958:3-6958:60)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6959:3-6959:23)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6960:7-6960:23)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6961:5-6961:53)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6857:3-6857:92)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6857:3-6857:92)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6418:3-6418:51)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6419:3-6419:17)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6423:5-6423:52)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6425:5-6425:63)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6427:7-6427:54)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6965:5-6966:45)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6819:3-6819:24)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6820:3-6820:20)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6821:3-6821:76)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6828:3-6828:22)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6829:3-6829:32)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6835:3-6835:61)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6451:11-6451:41)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6835:3-6835:61)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6831:5-6831:30)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6838:3-6838:30)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6968:7-6969:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6971:7-6971:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6972:7-6972:59)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6973:7-6973:55)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6973:7-6973:55)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6974:7-6974:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6975:7-6975:40)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6975:7-6975:40)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6295:3-6295:36)
[Warning][Unknown] lval (& tcmd)->hash_list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6295:3-6295:36)
[Warning][Unknown] lval (& tcmd)->hash_list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8206:3-8206:9)
[Warning][Unknown] lval (& tcmd)->hash_list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6296:3-6296:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6976:7-6976:60)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6976:7-6976:60)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6982:3-6982:40)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6802:3-6802:34)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6804:3-6804:73)
[Warning][Imprecise][Call] Function pointer *((shost->hostt)->transfer_response) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6804:3-6804:73)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6804:3-6804:73)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7465:3-7465:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7466:3-7467:84)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7007:3-7007:61)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7018:3-7018:80)
[Warning][Imprecise][Call] Function pointer *((shost->transportt)->tsk_mgmt_response) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7018:3-7018:80)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7018:3-7018:80)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7469:3-7469:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7470:3-7471:64)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7053:3-7053:61)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7064:3-7064:75)
[Warning][Imprecise][Call] Function pointer *((shost->transportt)->it_nexus_response) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7064:3-7064:75)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7064:3-7064:75)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7474:3-7474:80)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7495:3-7495:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7298:11-7298:83)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7513:3-7513:38)
[Info][Unsound] Unknown value in {&tx_ring.tr_lock.ldv_5961.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7513:3-7513:38)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7520:7-7520:42)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6351:3-6351:61)
[Info][Unsound] Unknown value in {&tx_ring.tr_lock.ldv_5961.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6351:3-6351:61)
[Warning][Unknown] lval (& ring)->tr_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6351:3-6351:61)
[Warning][Unknown] lval (& ring)->tr_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8239:3-8239:9)
[Warning][Unknown] lval (& ring)->tr_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6352:3-6352:9)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7740:7-7740:28)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7750:5-7750:26)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7643:3-7643:40)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7643:3-7643:40)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7643:3-7643:40)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7825:3-7825:30)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7825:3-7825:30)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7825:3-7825:30)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:12:1-12:219)
[Warning][Deadcode] Function 'INIT_LIST_HEAD' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6283:1-6290:1)
[Warning][Deadcode] Function 'list_move' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6301:1-6308:1)
[Warning][Deadcode] Function 'list_empty' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6309:1-6314:1)
[Warning][Deadcode] Function '__kmalloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6387:1-6390:1)
[Warning][Deadcode] Function 'kmalloc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6392:1-6398:1)
[Warning][Deadcode] Function 'kzalloc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6400:1-6406:1)
[Warning][Deadcode] Function 'scsi_host_get_command' is uncalled: 28 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6511:1-6560:1)
[Warning][Deadcode] Function 'cmd_hashlist_del' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6580:1-6596:1)
[Warning][Deadcode] Function 'init_scsi_tgt_cmd' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6620:1-6648:1)
[Warning][Deadcode] Function 'scsi_tgt_alloc_queue' is uncalled: 25 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6649:1-6694:1)
[Warning][Deadcode] Function 'scsi_tgt_free_queue' is uncalled: 37 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6695:1-6764:1)
[Warning][Deadcode] Function 'scsi_tgt_queue_command' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6772:1-6786:1)
[Warning][Deadcode] Function 'scsi_tgt_cmd_done' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6787:1-6796:1)
[Warning][Deadcode] Function 'scsi_tgt_tsk_mgmt_request' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6988:1-7001:1)
[Warning][Deadcode] Function 'scsi_tgt_it_nexus_create' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7024:1-7035:1)
[Warning][Deadcode] Function 'scsi_tgt_it_nexus_destroy' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7036:1-7047:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_1' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7176:1-7183:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7184:1-7191:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_3' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7192:1-7199:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_4' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7200:1-7207:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_5' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7208:1-7215:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_6' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7216:1-7227:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_7' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7228:1-7235:1)
[Warning][Deadcode] Function 'scsi_bufflen' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7270:1-7275:1)
[Warning][Deadcode] Function 'tgt_uspace_send_event' is uncalled: 20 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7301:1-7337:1)
[Warning][Deadcode] Function 'scsi_tgt_uspace_send_cmd' is uncalled: 20 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7338:1-7379:1)
[Warning][Deadcode] Function 'scsi_tgt_uspace_send_status' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7380:1-7401:1)
[Warning][Deadcode] Function 'scsi_tgt_uspace_send_tsk_mgmt' is uncalled: 14 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7402:1-7430:1)
[Warning][Deadcode] Function 'scsi_tgt_uspace_send_it_nexus_request' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7431:1-7453:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_15' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7761:1-7768:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_16' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7769:1-7776:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_17' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7777:1-7784:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_18' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7785:1-7796:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_19' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7797:1-7804:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_20' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7805:1-7812:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_21' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7813:1-7820:1)
[Warning][Deadcode] Function 'ldv_error' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7842:1-7847:1)
[Warning][Deadcode] Function 'ldv__builtin_trap' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7855:1-7861:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_interruptible_cred_guard_mutex_of_signal_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7863:1-7878:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_killable_cred_guard_mutex_of_signal_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7879:1-7894:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_cred_guard_mutex_of_signal_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7895:1-7905:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_cred_guard_mutex_of_signal_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7906:1-7921:1)
[Warning][Deadcode] Function 'ldv_atomic_dec_and_mutex_lock_cred_guard_mutex_of_signal_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7922:1-7938:1)
[Warning][Deadcode] Function 'ldv_mutex_is_locked_cred_guard_mutex_of_signal_struct' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7939:1-7953:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_cred_guard_mutex_of_signal_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7954:1-7964:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_interruptible_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7966:1-7981:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_killable_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7982:1-7997:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_lock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7998:1-8008:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8009:1-8024:1)
[Warning][Deadcode] Function 'ldv_atomic_dec_and_mutex_lock_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8025:1-8040:1)
[Warning][Deadcode] Function 'ldv_mutex_is_locked_lock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8041:1-8055:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_lock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8056:1-8066:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_interruptible_mutex_of_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8068:1-8083:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_killable_mutex_of_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8084:1-8099:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_mutex_of_device' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8100:1-8110:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_mutex_of_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8111:1-8126:1)
[Warning][Deadcode] Function 'ldv_atomic_dec_and_mutex_lock_mutex_of_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8127:1-8142:1)
[Warning][Deadcode] Function 'ldv_mutex_is_locked_mutex_of_device' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8143:1-8157:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_mutex_of_device' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8158:1-8168:1)
[Warning][Deadcode] Function '__init_work' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8202:1-8204:1)
[Warning][Deadcode] Function '__list_del_entry' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8208:1-8210:1)
[Warning][Deadcode] Function '__scsi_alloc_queue' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8218:1-8220:1)
[Warning][Deadcode] Function '__scsi_get_command' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8221:1-8223:1)
[Warning][Deadcode] Function '__wake_up' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8227:1-8229:1)
[Warning][Deadcode] Function 'blk_cleanup_queue' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8241:1-8243:1)
[Warning][Deadcode] Function 'blk_get_request' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8244:1-8246:1)
[Warning][Deadcode] Function 'blk_put_request' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8247:1-8249:1)
[Warning][Deadcode] Function 'blk_queue_dma_alignment' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8250:1-8252:1)
[Warning][Deadcode] Function 'get_device' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8267:1-8269:1)
[Warning][Deadcode] Function 'kmem_cache_alloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8274:1-8276:1)
[Warning][Deadcode] Function 'lockdep_init_map' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8293:1-8295:1)
[Warning][Deadcode] Function 'mutex_lock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8307:1-8309:1)
[Warning][Deadcode] Function 'mutex_trylock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8311:1-8313:1)
[Warning][Deadcode] Function 'mutex_unlock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8314:1-8316:1)
[Warning][Deadcode] Function 'put_device' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8325:1-8327:1)
[Warning][Deadcode] Function 'queue_work' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8329:1-8331:1)
[Warning][Deadcode] Function 'kfree' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8353:1-8355:1)
[Warning][Deadcode] Function 'ldv_check_final_state' has dead code:
  on line 8183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8183-8183)
  on line 8187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8187-8187)
  on line 8191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8191-8191)
[Warning][Deadcode] Function 'poll_wait' has dead code:
  on line 7264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7264-7264)
[Warning][Deadcode] Function 'tgt_poll' has dead code:
  on line 7515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7515-7515)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 467
  dead: 427 (422 in uncalled functions)
  total lines: 894
[Warning][Deadcode][CWE-570] condition 'ring->tr_idx != 0U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7514:7-7514:25)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_0 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7133:7-7133:32)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_cred_guard_mutex_of_signal_struct == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8181:7-8181:55)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_lock == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8185:7-8185:26)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_mutex_of_device == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:8189:7-8189:37)
[Warning][Deadcode][CWE-571] condition 'ldv_retval_0 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7738:9-7738:26)
[Warning][Deadcode][CWE-570] condition '(unsigned long )p != (unsigned long )((poll_table *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:7261:8-7263:230)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 0L' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--scsi--scsi_tgt.ko-main.cil.out.i:6431:11-6431:24)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
[Warning][Unsound][Call] No suitable function to call
