./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.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] malloc wrapper: ldv_malloc
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7214:3-7214:98)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6961:3-6961:62)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6961:3-6961:62)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6961:3-6961:62)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7782:3-7782:48)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7782:3-7782:48)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7782:3-7782:48)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7784:3-7784:70)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7784:3-7784:70)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7784:3-7784:70)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7328:5-7328:83)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7328:5-7328:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7328:5-7328:83)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7200:3-7200:24)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7200:3-7200:24)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7200:3-7200:24)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7201:3-7201:52)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7201:3-7201:52)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7201:3-7201:52)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7056:5-7056:27)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7056:5-7056:27)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7056:5-7056:27)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7154:3-7155:70)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4946:3-4946:42)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4946:3-4946:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4947:3-4947:56)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4947:3-4947:56)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4948:3-4948:34)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7148:3-7148:95)
[Warning][Unknown] lval (& card)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4632:11-4632:36)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6876:3-6876:35)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6876:3-6876:35)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7751:3-7751:81)
[Warning][Unknown] lval (& host)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7751:3-7751:81)
[Warning][Unknown] lval (& host)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9989:3-9989:128)
[Warning][Unknown] lval (& host)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11839:3-11839:9)
[Warning][Unknown] lval (& host)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9992:3-9992:9)
[Warning][Unknown] lval (& host)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7753:3-7753:9)
[Warning][Unknown] lval (& card)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4638:3-4638:26)
[Warning][Unknown] lval (& card)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4639:3-4639:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6453:3-6453:21)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6454:3-6454:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6466:3-6466:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6047:3-6047:50)
[Warning][Unknown] lval (& card)->current_mrq points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12441:3-12441:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6049:3-6049:31)
[Warning][Unknown] lval (& card)->mrq_complete points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11188:3-11188:142)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6928:3-6928:37)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6928:3-6928:37)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7760:3-7760:83)
[Warning][Unknown] lval (& host)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7760:3-7760:83)
[Warning][Unknown] lval (& host)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10064:3-10064:134)
[Warning][Unknown] lval (& host)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11863:3-11863:9)
[Warning][Unknown] lval (& host)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10067:3-10067:9)
[Warning][Unknown] lval (& host)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7762:3-7762:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6929:3-6929:71)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10905:3-10905:139)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12258:3-12258:9)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10906:3-10906:85)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9577:3-9577:9)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7770:3-7770:63)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12374:3-12374:9)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7772:3-7772:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6930:3-6930:30)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6931:3-6931:55)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10916:3-10916:141)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12282:3-12282:9)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10917:3-10917:85)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7458:3-7458:38)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4571:3-4571:71)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4571:3-4571:71)
[Info][Unsound] Unknown value in {&(alloc@sid:1236).q_lock.__annonCompField18.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4571:3-4571:71)
[Info][Unsound] Unknown value in {&(alloc@sid:1309).q_lock.__annonCompField18.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4571:3-4571:71)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4571:3-4571:71)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12380:3-12380:9)
[Warning][Unknown] lval (& lock)->__annonCompField18.rlock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12380:3-12380:9)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4573:3-4573:9)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7460:3-7460:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7142:3-7143:66)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6848:3-6848:71)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7742:3-7742:63)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7744:3-7744:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6849:3-6849:29)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6850:3-6850:19)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6851:3-6851:55)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7088:7-7090:83)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7088:7-7090:83)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4879:3-4879:54)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4884:5-4884:45)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4564:11-4564:44)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6759:3-6760:32)
[Info][Unsound] Unknown value in {&(alloc@sid:1236).q_lock.__annonCompField18.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6759:3-6760:32)
[Warning][Unknown] lval (& msb)->q_lock.__annonCompField18.rlock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12377:3-12377:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7170:5-7171:96)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7170:5-7171:96)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4907:3-4907:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4907:3-4907:42)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4912:7-4912:47)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4917:7-4917:31)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)p in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12489:3-12489:18)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6807:3-6807:71)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7685:3-7685:63)
[Warning][Unknown] lval (& msb)->q_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7687:3-7687:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6808:3-6808:18)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6809:3-6809:30)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6810:3-6810:55)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6811:3-6811:33)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7228:5-7228:80)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6976:3-6976:59)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6976:3-6976:59)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6976:3-6976:59)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7794:3-7794:44)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7794:3-7794:44)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7794:3-7794:44)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7795:3-7795:59)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7795:3-7795:59)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7795:3-7795:59)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7346:3-7346:83)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7346:3-7346:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7346:3-7346:83)
[Warning][Deadcode] Function 'ldv_check_alloc_nonatomic' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4405:1-4414:1)
[Warning][Deadcode] Function 'ldv_check_for_read_section' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4425:1-4436:1)
[Warning][Deadcode] Function 'ldv_create_class' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4438:1-4454:1)
[Warning][Deadcode] Function 'ldv_register_class' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4455:1-4471:1)
[Warning][Deadcode] Function '__fswab16' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4504:1-4509:1)
[Warning][Deadcode] Function '__fswab32' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4510:1-4519:1)
[Warning][Deadcode] Function '__swab16p' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4520:1-4529:1)
[Warning][Deadcode] Function '__be16_to_cpup' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4530:1-4539:1)
[Warning][Deadcode] Function 'kobject_name' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4609:1-4614:1)
[Warning][Deadcode] Function 'dev_name' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4615:1-4628:1)
[Warning][Deadcode] Function 'set_capacity' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4654:1-4660:1)
[Warning][Deadcode] Function 'bio_has_data' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4666:1-4675:1)
[Warning][Deadcode] Function 'bio_cur_bytes' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4676:1-4697:1)
[Warning][Deadcode] Function 'blk_rq_pos' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4700:1-4705:1)
[Warning][Deadcode] Function 'blk_rq_bytes' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4706:1-4711:1)
[Warning][Deadcode] Function 'blk_rq_cur_bytes' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4712:1-4727:1)
[Warning][Deadcode] Function 'sg_assign_page' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4746:1-4790:1)
[Warning][Deadcode] Function 'sg_set_page' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4791:1-4802:1)
[Warning][Deadcode] Function 'sg_page' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4803:1-4832:1)
[Warning][Deadcode] Function 'mspro_from_sysfs_attr' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4955:1-4966:1)
[Warning][Deadcode] Function 'mspro_block_attr_name' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4967:1-5025:1)
[Warning][Deadcode] Function 'mspro_block_attr_show_default' is uncalled: 16 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5026:1-5064:1)
[Warning][Deadcode] Function 'mspro_block_attr_show_sysinfo' is uncalled: 77 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5065:1-5220:1)
[Warning][Deadcode] Function 'mspro_block_attr_show_modelname' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5221:1-5235:1)
[Warning][Deadcode] Function 'mspro_block_attr_show_mbr' is uncalled: 25 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5236:1-5292:1)
[Warning][Deadcode] Function 'mspro_block_attr_show_specfile' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5293:1-5345:1)
[Warning][Deadcode] Function 'mspro_block_attr_show_devinfo' is uncalled: 20 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5346:1-5392:1)
[Warning][Deadcode] Function 'mspro_block_attr_show' is uncalled: 20 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5393:1-5438:1)
[Warning][Deadcode] Function 'h_mspro_block_req_init' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5439:1-5452:1)
[Warning][Deadcode] Function 'h_mspro_block_default' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5453:1-5462:1)
[Warning][Deadcode] Function 'h_mspro_block_default_bad' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5463:1-5468:1)
[Warning][Deadcode] Function 'h_mspro_block_get_ro' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5469:1-5492:1)
[Warning][Deadcode] Function 'h_mspro_block_wait_for_ced' is uncalled: 16 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5493:1-5530:1)
[Warning][Deadcode] Function 'h_mspro_block_transfer_data' is uncalled: 66 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5531:1-5670:1)
[Warning][Deadcode] Function 'h_mspro_block_setup_cmd' is uncalled: 16 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5671:1-5700:1)
[Warning][Deadcode] Function 'mspro_block_issue_req' is uncalled: 54 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5701:1-5810:1)
[Warning][Deadcode] Function 'mspro_block_complete_req' is uncalled: 52 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5811:1-5923:1)
[Warning][Deadcode] Function 'mspro_block_stop' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5924:1-5961:1)
[Warning][Deadcode] Function 'mspro_block_start' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5962:1-5977:1)
[Warning][Deadcode] Function 'mspro_block_prepare_req' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5978:1-5991:1)
[Warning][Deadcode] Function 'mspro_block_submit_req' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:5992:1-6037:1)
[Warning][Deadcode] Function 'mspro_block_set_interface' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6055:1-6078:1)
[Warning][Deadcode] Function 'mspro_block_switch_interface' is uncalled: 50 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6079:1-6183:1)
[Warning][Deadcode] Function 'mspro_block_read_attributes' is uncalled: 125 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6184:1-6433:1)
[Warning][Deadcode] Function 'mspro_block_init_disk' is uncalled: 80 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6553:1-6697:1)
[Warning][Deadcode] Function 'mspro_block_check_card' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6727:1-6738:1)
[Warning][Deadcode] Function 'kmalloc' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7352:1-7363:1)
[Warning][Deadcode] Function 'kcalloc' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7365:1-7376:1)
[Warning][Deadcode] Function 'ldv_put_disk_99' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7424:1-7433:1)
[Warning][Deadcode] Function 'ldv___ldv_linux_kernel_locking_spinlock_spin_lock_101' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7443:1-7452:1)
[Warning][Deadcode] Function 'ldv___ldv_linux_kernel_locking_spinlock_spin_lock_103' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7463:1-7472:1)
[Warning][Deadcode] Function 'ldv_wait_for_completion_105' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7473:1-7482:1)
[Warning][Deadcode] Function 'ldv___ldv_linux_kernel_locking_spinlock_spin_lock_106' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7483:1-7492:1)
[Warning][Deadcode] Function 'ldv_wait_for_completion_109' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7503:1-7512:1)
[Warning][Deadcode] Function 'ldv_wait_for_completion_110' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7513:1-7522:1)
[Warning][Deadcode] Function 'ldv_wait_for_completion_111' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7523:1-7532:1)
[Warning][Deadcode] Function 'ldv_wait_for_completion_112' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7533:1-7542:1)
[Warning][Deadcode] Function 'ldv_wait_for_completion_113' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7543:1-7552:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_114' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7553:1-7561:1)
[Warning][Deadcode] Function 'ldv_idr_alloc_115' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7562:1-7573:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_116' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7574:1-7582:1)
[Warning][Deadcode] Function 'ldv_alloc_disk_117' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7583:1-7597:1)
[Warning][Deadcode] Function 'ldv_blk_init_queue_118' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7598:1-7613:1)
[Warning][Deadcode] Function 'ldv_add_disk_119' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7614:1-7623:1)
[Warning][Deadcode] Function 'ldv_put_disk_120' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7624:1-7633:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_121' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7634:1-7642:1)
[Warning][Deadcode] Function 'ldv_idr_remove_122' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7643:1-7651:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_123' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7652:1-7660:1)
[Warning][Deadcode] Function 'ldv_sysfs_create_group_124' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7661:1-7670:1)
[Warning][Deadcode] Function 'ldv_sysfs_remove_group_125' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7671:1-7679:1)
[Warning][Deadcode] Function 'ldv_blk_cleanup_queue_129' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7700:1-7709:1)
[Warning][Deadcode] Function 'ldv_sysfs_remove_group_130' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7710:1-7718:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_131' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7719:1-7727:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_132' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7728:1-7736:1)
[Warning][Deadcode] Function 'ldv_ldv_check_final_state_144' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7849:1-7876:1)
[Warning][Deadcode] Function 'ldv_linux_alloc_irq_check_alloc_nonatomic' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7908:1-7923:1)
[Warning][Deadcode] Function 'ldv_linux_alloc_spinlock_check_alloc_flags' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7927:1-7940:1)
[Warning][Deadcode] Function 'ldv_linux_alloc_spinlock_check_alloc_nonatomic' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7941:1-7951:1)
[Warning][Deadcode] Function 'ldv_linux_alloc_usb_lock_check_alloc_nonatomic' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7967:1-7975:1)
[Warning][Deadcode] Function 'ldv_linux_alloc_usb_lock_usb_lock_device' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7976:1-7982:1)
[Warning][Deadcode] Function 'ldv_linux_alloc_usb_lock_usb_trylock_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7983:1-8001:1)
[Warning][Deadcode] Function 'ldv_linux_alloc_usb_lock_usb_lock_device_for_reset' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8002:1-8020:1)
[Warning][Deadcode] Function 'ldv_linux_alloc_usb_lock_usb_unlock_device' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8021:1-8027:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_atomic_add' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8028:1-8034:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_atomic_sub' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8035:1-8041:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_atomic_sub_and_test' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8042:1-8052:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_atomic_inc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8053:1-8059:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_atomic_dec' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8060:1-8066:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_atomic_dec_and_test' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8067:1-8077:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_atomic_inc_and_test' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8078:1-8088:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_atomic_add_return' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8089:1-8095:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_atomic_add_negative' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8096:1-8102:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_atomic_inc_short' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8103:1-8109:1)
[Warning][Deadcode] Function 'ldv_linux_arch_io_io_mem_remap' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8113:1-8129:1)
[Warning][Deadcode] Function 'ldv_linux_arch_io_io_mem_unmap' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8130:1-8139:1)
[Warning][Deadcode] Function 'ldv_linux_block_genhd_alloc_disk' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8155:1-8172:1)
[Warning][Deadcode] Function 'ldv_linux_block_genhd_add_disk' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8173:1-8182:1)
[Warning][Deadcode] Function 'ldv_linux_block_genhd_put_disk' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8193:1-8205:1)
[Warning][Deadcode] Function 'ldv_linux_block_queue_request_queue' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8219:1-8236:1)
[Warning][Deadcode] Function 'ldv_linux_block_queue_blk_cleanup_queue' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8237:1-8246:1)
[Warning][Deadcode] Function 'ldv_linux_block_request_blk_get_request' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8261:1-8283:1)
[Warning][Deadcode] Function 'ldv_linux_block_request_blk_make_request' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8284:1-8303:1)
[Warning][Deadcode] Function 'ldv_linux_block_request_put_blk_rq' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8304:1-8313:1)
[Warning][Deadcode] Function 'ldv_linux_drivers_base_class_create_class' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8328:1-8347:1)
[Warning][Deadcode] Function 'ldv_linux_drivers_base_class_register_class' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8348:1-8364:1)
[Warning][Deadcode] Function 'ldv_linux_drivers_base_class_unregister_class' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8365:1-8374:1)
[Warning][Deadcode] Function 'ldv_linux_drivers_base_class_destroy_class' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8375:1-8395:1)
[Warning][Deadcode] Function 'ldv_dev_get_drvdata' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8406:1-8415:1)
[Warning][Deadcode] Function 'ldv_dev_set_drvdata' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8416:1-8427:1)
[Warning][Deadcode] Function 'ldv_spi_alloc_master' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8428:1-8446:1)
[Warning][Deadcode] Function 'ldv_err_ptr' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8453:1-8458:1)
[Warning][Deadcode] Function 'ldv_ptr_err' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8459:1-8464:1)
[Warning][Deadcode] Function 'ldv_is_err_or_null' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8465:1-8484:1)
[Warning][Deadcode] Function 'ldv_linux_fs_char_dev_register_chrdev' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8489:1-8512:1)
[Warning][Deadcode] Function 'ldv_linux_fs_char_dev_register_chrdev_region' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8513:1-8529:1)
[Warning][Deadcode] Function 'ldv_linux_fs_char_dev_unregister_chrdev_region' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8530:1-8539:1)
[Warning][Deadcode] Function 'ldv_linux_fs_sysfs_sysfs_create_group' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8552:1-8568:1)
[Warning][Deadcode] Function 'ldv_linux_fs_sysfs_sysfs_remove_group' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8569:1-8578:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_rwlock_read_lock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8596:1-8605:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_rwlock_read_unlock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8606:1-8615:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_rwlock_write_lock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8616:1-8625:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_rwlock_write_unlock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8626:1-8635:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_rwlock_read_trylock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8636:1-8654:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_rwlock_write_trylock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8655:1-8673:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_module_module_get' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8687:1-8696:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_module_try_module_get' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8697:1-8715:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_module_module_put' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8716:1-8728:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_module_module_put_and_exit' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8729:1-8738:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_module_module_refcount' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8739:1-8744:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_rcu_srcu_srcu_read_lock' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8758:1-8764:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_rcu_srcu_srcu_read_unlock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8765:1-8774:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_rcu_srcu_check_for_read_section' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8775:1-8783:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_rcu_update_lock_bh_rcu_read_lock_bh' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8797:1-8803:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_rcu_update_lock_bh_rcu_read_unlock_bh' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8804:1-8813:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_rcu_update_lock_bh_check_for_read_section' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8814:1-8822:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_rcu_update_lock_sched_rcu_read_lock_sched' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8836:1-8842:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_rcu_update_lock_sched_rcu_read_unlock_sched' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8843:1-8852:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_rcu_update_lock_sched_check_for_read_section' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8853:1-8861:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_rcu_update_lock_rcu_read_lock' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8875:1-8881:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_rcu_update_lock_rcu_read_unlock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8882:1-8891:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_rcu_update_lock_check_for_read_section' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8892:1-8900:1)
[Warning][Deadcode] Function 'ldv_post_probe' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8930:1-8939:1)
[Warning][Deadcode] Function 'ldv_switch_to_interrupt_context' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8953:1-8959:1)
[Warning][Deadcode] Function 'ldv_switch_to_process_context' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8960:1-8966:1)
[Warning][Deadcode] Function 'ldv_linux_lib_find_bit_find_next_bit' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8976:1-8990:1)
[Warning][Deadcode] Function 'ldv_linux_lib_find_bit_find_first_bit' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8991:1-9004:1)
[Warning][Deadcode] Function 'ldv_linux_mmc_sdio_func_check_context' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9031:1-9039:1)
[Warning][Deadcode] Function 'ldv_linux_mmc_sdio_func_sdio_claim_host' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9040:1-9049:1)
[Warning][Deadcode] Function 'ldv_linux_mmc_sdio_func_sdio_release_host' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9050:1-9059:1)
[Warning][Deadcode] Function 'ldv_pre_register_netdev' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9072:1-9088:1)
[Warning][Deadcode] Function 'ldv_linux_net_register_check_return_value_probe' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9096:1-9110:1)
[Warning][Deadcode] Function 'ldv_linux_net_rtnetlink_past_rtnl_unlock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9115:1-9124:1)
[Warning][Deadcode] Function 'ldv_linux_net_rtnetlink_past_rtnl_lock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9125:1-9134:1)
[Warning][Deadcode] Function 'ldv_linux_net_rtnetlink_before_ieee80211_unregister_hw' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9135:1-9144:1)
[Warning][Deadcode] Function 'ldv_linux_net_rtnetlink_rtnl_is_locked' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9145:1-9162:1)
[Warning][Deadcode] Function 'ldv_linux_net_rtnetlink_rtnl_trylock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9163:1-9178:1)
[Warning][Deadcode] Function 'ldv_linux_net_sock_past_lock_sock_nested' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9191:1-9197:1)
[Warning][Deadcode] Function 'ldv_linux_net_sock_lock_sock_fast' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9198:1-9212:1)
[Warning][Deadcode] Function 'ldv_linux_net_sock_unlock_sock_fast' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9213:1-9222:1)
[Warning][Deadcode] Function 'ldv_linux_net_sock_before_release_sock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9223:1-9232:1)
[Warning][Deadcode] Function 'ldv_linux_usb_coherent_usb_alloc_coherent' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9245:1-9261:1)
[Warning][Deadcode] Function 'ldv_linux_usb_coherent_usb_free_coherent' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9262:1-9274:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_usb_get_dev' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9289:1-9298:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_usb_put_dev' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9299:1-9316:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_check_return_value_probe' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9317:1-9328:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_initialize' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9329:1-9335:1)
[Warning][Deadcode] Function 'ldv_linux_usb_dev_check_final_state' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9336:1-9344:1)
[Warning][Deadcode] Function 'ldv_linux_usb_gadget_create_class' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9353:1-9369:1)
[Warning][Deadcode] Function 'ldv_linux_usb_gadget_register_class' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9370:1-9385:1)
[Warning][Deadcode] Function 'ldv_linux_usb_gadget_unregister_class' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9386:1-9394:1)
[Warning][Deadcode] Function 'ldv_linux_usb_gadget_destroy_class' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9395:1-9415:1)
[Warning][Deadcode] Function 'ldv_linux_usb_gadget_register_chrdev' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9416:1-9438:1)
[Warning][Deadcode] Function 'ldv_linux_usb_gadget_register_chrdev_region' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9439:1-9454:1)
[Warning][Deadcode] Function 'ldv_linux_usb_gadget_unregister_chrdev_region' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9455:1-9463:1)
[Warning][Deadcode] Function 'ldv_linux_usb_gadget_register_usb_gadget' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9464:1-9480:1)
[Warning][Deadcode] Function 'ldv_linux_usb_gadget_unregister_usb_gadget' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9481:1-9490:1)
[Warning][Deadcode] Function 'ldv_pre_usb_register_driver' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9503:1-9519:1)
[Warning][Deadcode] Function 'ldv_linux_usb_register_check_return_value_probe' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9527:1-9541:1)
[Warning][Deadcode] Function 'ldv_linux_usb_urb_usb_free_urb' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9545:1-9557:1)
[Warning][Deadcode] Function 'ldv__builtin_expect' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9587:1-9592:1)
[Warning][Deadcode] Function 'ldv__builtin_trap' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9593:1-9601:1)
[Warning][Deadcode] Function 'ldv_malloc' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9606:1-9629:1)
[Warning][Deadcode] Function 'ldv_xzalloc' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9689:1-9704:1)
[Warning][Deadcode] Function 'ldv_undef_ulong' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9718:1-9727:1)
[Warning][Deadcode] Function 'ldv_undef_int_negative' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9728:1-9740:1)
[Warning][Deadcode] Function 'ldv_undef_int_nonpositive' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9741:1-9753:1)
[Warning][Deadcode] Function 'ldv_thread_create' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9760:1-9772:1)
[Warning][Deadcode] Function 'ldv_thread_create_N' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9773:1-9795:1)
[Warning][Deadcode] Function 'ldv_thread_join' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9796:1-9801:1)
[Warning][Deadcode] Function 'ldv_thread_join_N' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9802:1-9807:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_lock_i_mutex_of_inode' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9813:1-9822:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_lock_interruptible_or_killable_i_mutex_of_inode' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9823:1-9838:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_is_locked_i_mutex_of_inode' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9839:1-9856:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_trylock_i_mutex_of_inode' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9857:1-9872:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_atomic_dec_and_mutex_lock_i_mutex_of_inode' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9873:1-9887:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_unlock_i_mutex_of_inode' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9888:1-9897:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_lock_lock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9899:1-9908:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_lock_interruptible_or_killable_lock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9909:1-9924:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_is_locked_lock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9925:1-9942:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_trylock_lock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9943:1-9958:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_atomic_dec_and_mutex_lock_lock' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9959:1-9973:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_unlock_lock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9974:1-9983:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_lock_interruptible_or_killable_lock_of_memstick_host' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:9995:1-10010:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_is_locked_lock_of_memstick_host' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10011:1-10028:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_trylock_lock_of_memstick_host' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10029:1-10044:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_atomic_dec_and_mutex_lock_lock_of_memstick_host' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10045:1-10059:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_lock_interruptible_or_killable_mspro_block_disk_lock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10081:1-10096:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_is_locked_mspro_block_disk_lock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10097:1-10114:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_trylock_mspro_block_disk_lock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10115:1-10130:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_atomic_dec_and_mutex_lock_mspro_block_disk_lock' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10131:1-10145:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_lock_mutex_of_device' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10157:1-10166:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_lock_interruptible_or_killable_mutex_of_device' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10167:1-10182:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_is_locked_mutex_of_device' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10183:1-10200:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_trylock_mutex_of_device' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10201:1-10216:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_atomic_dec_and_mutex_lock_mutex_of_device' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10217:1-10231:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_unlock_mutex_of_device' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10232:1-10241:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_initialize' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10242:1-10252:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_check_final_state' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10253:1-10265:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_lock_alloc_lock_of_task_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10271:1-10281:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_alloc_lock_of_task_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10282:1-10292:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_trylock_alloc_lock_of_task_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10293:1-10309:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_wait_alloc_lock_of_task_struct' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10310:1-10319:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_locked_alloc_lock_of_task_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10320:1-10333:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_can_lock_alloc_lock_of_task_struct' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10334:1-10343:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_contended_alloc_lock_of_task_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10344:1-10357:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_atomic_dec_and_lock_alloc_lock_of_task_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10358:1-10374:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_lock_i_lock_of_inode' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10376:1-10386:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_i_lock_of_inode' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10387:1-10397:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_trylock_i_lock_of_inode' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10398:1-10414:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_wait_i_lock_of_inode' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10415:1-10424:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_locked_i_lock_of_inode' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10425:1-10438:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_can_lock_i_lock_of_inode' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10439:1-10448:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_contended_i_lock_of_inode' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10449:1-10462:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_atomic_dec_and_lock_i_lock_of_inode' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10463:1-10479:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_lock_lock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10481:1-10491:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_lock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10492:1-10502:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_trylock_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10503:1-10519:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_wait_lock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10520:1-10529:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_locked_lock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10530:1-10543:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_can_lock_lock' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10544:1-10553:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_contended_lock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10554:1-10567:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_atomic_dec_and_lock_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10568:1-10584:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_lock_lock_of_NOT_ARG_SIGN' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10586:1-10596:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_lock_of_NOT_ARG_SIGN' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10597:1-10607:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_trylock_lock_of_NOT_ARG_SIGN' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10608:1-10624:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_wait_lock_of_NOT_ARG_SIGN' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10625:1-10634:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_locked_lock_of_NOT_ARG_SIGN' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10635:1-10648:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_can_lock_lock_of_NOT_ARG_SIGN' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10649:1-10658:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_contended_lock_of_NOT_ARG_SIGN' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10659:1-10672:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_atomic_dec_and_lock_lock_of_NOT_ARG_SIGN' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10673:1-10689:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_lock_node_size_lock_of_pglist_data' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10691:1-10701:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_node_size_lock_of_pglist_data' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10702:1-10712:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_trylock_node_size_lock_of_pglist_data' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10713:1-10729:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_wait_node_size_lock_of_pglist_data' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10730:1-10739:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_locked_node_size_lock_of_pglist_data' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10740:1-10753:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_can_lock_node_size_lock_of_pglist_data' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10754:1-10763:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_contended_node_size_lock_of_pglist_data' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10764:1-10777:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_atomic_dec_and_lock_node_size_lock_of_pglist_data' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10778:1-10794:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_lock_ptl' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10796:1-10806:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_ptl' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10807:1-10817:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_trylock_ptl' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10818:1-10834:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_wait_ptl' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10835:1-10844:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_locked_ptl' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10845:1-10858:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_can_lock_ptl' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10859:1-10868:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_contended_ptl' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10869:1-10882:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_atomic_dec_and_lock_ptl' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10883:1-10899:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_trylock_q_lock_of_mspro_block_data' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10923:1-10939:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_wait_q_lock_of_mspro_block_data' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10940:1-10949:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_locked_q_lock_of_mspro_block_data' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10950:1-10963:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_can_lock_q_lock_of_mspro_block_data' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10964:1-10973:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_contended_q_lock_of_mspro_block_data' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10974:1-10987:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_atomic_dec_and_lock_q_lock_of_mspro_block_data' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:10988:1-11004:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_lock_siglock_of_sighand_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11006:1-11016:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_siglock_of_sighand_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11017:1-11027:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_trylock_siglock_of_sighand_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11028:1-11044:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_wait_siglock_of_sighand_struct' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11045:1-11054:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_locked_siglock_of_sighand_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11055:1-11068:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_can_lock_siglock_of_sighand_struct' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11069:1-11078:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_contended_siglock_of_sighand_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11079:1-11092:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_atomic_dec_and_lock_siglock_of_sighand_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11093:1-11109:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_check_final_state' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11110:1-11125:1)
[Warning][Deadcode] Function 'ldv_exclusive_spin_is_locked' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11126:1-11163:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_sched_completion_init_completion_mrq_complete_of_memstick_dev' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11167:1-11173:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_sched_completion_init_completion_macro_mrq_complete_of_memstick_dev' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11174:1-11183:1)
[Warning][Deadcode] Function 'ldv_linux_lib_idr_idr_init_mspro_block_disk_idr' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11199:1-11208:1)
[Warning][Deadcode] Function 'ldv_linux_lib_idr_idr_alloc_mspro_block_disk_idr' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11209:1-11219:1)
[Warning][Deadcode] Function 'ldv_linux_lib_idr_idr_find_mspro_block_disk_idr' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11220:1-11230:1)
[Warning][Deadcode] Function 'ldv_assert_linux_net_rtnetlink__double_lock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11274:1-11285:1)
[Warning][Deadcode] Function 'ldv_assert_linux_net_rtnetlink__double_unlock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11298:1-11309:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_rwlock__read_lock_on_write_lock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11311:1-11322:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_rwlock__more_read_unlocks' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11323:1-11334:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_rwlock__double_write_lock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11347:1-11358:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_rwlock__double_write_unlock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11359:1-11370:1)
[Warning][Deadcode] Function 'ldv_assert_linux_lib_idr__double_init' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11384:1-11395:1)
[Warning][Deadcode] Function 'ldv_assert_linux_lib_idr__destroyed_before_usage' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11408:1-11419:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_sched_completion__double_init' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11433:1-11444:1)
[Warning][Deadcode] Function 'ldv_assert_linux_net_register__wrong_return_value' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11458:1-11469:1)
[Warning][Deadcode] Function 'ldv_assert_linux_fs_char_dev__double_registration' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11471:1-11482:1)
[Warning][Deadcode] Function 'ldv_assert_linux_fs_char_dev__double_deregistration' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11483:1-11494:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_srcu__more_unlocks' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11508:1-11519:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_srcu__locked_at_read_section' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11520:1-11531:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_module__less_initial_decrement' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11545:1-11556:1)
[Warning][Deadcode] Function 'ldv_assert_linux_alloc_spinlock__wrong_flags' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11570:1-11581:1)
[Warning][Deadcode] Function 'ldv_assert_linux_alloc_spinlock__nonatomic' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11582:1-11593:1)
[Warning][Deadcode] Function 'ldv_assert_linux_lib_find_bit__offset_out_of_range' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11595:1-11606:1)
[Warning][Deadcode] Function 'ldv_assert_linux_mmc_sdio_func__wrong_params' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11608:1-11619:1)
[Warning][Deadcode] Function 'ldv_assert_linux_mmc_sdio_func__double_claim' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11620:1-11631:1)
[Warning][Deadcode] Function 'ldv_assert_linux_mmc_sdio_func__release_without_claim' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11632:1-11643:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_coherent__less_initial_decrement' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11657:1-11668:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_update_lock__more_unlocks' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11682:1-11693:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_update_lock__locked_at_read_section' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11694:1-11705:1)
[Warning][Deadcode] Function 'ldv_assert_linux_net_sock__double_release' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11731:1-11742:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_update_lock_bh__more_unlocks' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11744:1-11755:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_update_lock_bh__locked_at_read_section' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11756:1-11767:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_dev__unincremented_counter_decrement' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11781:1-11792:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_dev__less_initial_decrement' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11793:1-11804:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_dev__more_initial_at_exit' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11805:1-11816:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_dev__probe_failed' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11817:1-11828:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_mutex__one_thread_double_lock_try' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11842:1-11853:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_mutex__one_thread_locked_at_exit' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11866:1-11877:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_gadget__class_registration_with_usb_gadget' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11879:1-11890:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_gadget__class_deregistration_with_usb_gadget' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11891:1-11902:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_gadget__chrdev_registration_with_usb_gadget' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11903:1-11914:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_gadget__chrdev_deregistration_with_usb_gadget' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11915:1-11926:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_gadget__double_usb_gadget_registration' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11927:1-11938:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_gadget__double_usb_gadget_deregistration' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11939:1-11950:1)
[Warning][Deadcode] Function 'ldv_assert_linux_alloc_usb_lock__wrong_flags' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11964:1-11975:1)
[Warning][Deadcode] Function 'ldv_assert_linux_alloc_usb_lock__nonatomic' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11976:1-11987:1)
[Warning][Deadcode] Function 'ldv_assert_linux_block_request__double_get' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11989:1-12000:1)
[Warning][Deadcode] Function 'ldv_assert_linux_block_request__double_put' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12001:1-12012:1)
[Warning][Deadcode] Function 'ldv_assert_linux_alloc_irq__nonatomic' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12038:1-12049:1)
[Warning][Deadcode] Function 'ldv_assert_linux_drivers_base_class__double_registration' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12051:1-12062:1)
[Warning][Deadcode] Function 'ldv_assert_linux_drivers_base_class__double_deregistration' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12063:1-12074:1)
[Warning][Deadcode] Function 'ldv_assert_linux_block_queue__double_allocation' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12088:1-12099:1)
[Warning][Deadcode] Function 'ldv_assert_linux_block_queue__use_before_allocation' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12100:1-12111:1)
[Warning][Deadcode] Function 'ldv_assert_linux_block_genhd__double_allocation' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12125:1-12136:1)
[Warning][Deadcode] Function 'ldv_assert_linux_block_genhd__use_before_allocation' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12137:1-12148:1)
[Warning][Deadcode] Function 'ldv_assert_linux_block_genhd__free_before_allocation' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12161:1-12172:1)
[Warning][Deadcode] Function 'ldv_assert_linux_arch_io__less_initial_decrement' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12186:1-12197:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_register__wrong_return_value' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12211:1-12222:1)
[Warning][Deadcode] Function 'ldv_assert_linux_fs_sysfs__less_initial_decrement' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12224:1-12235:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_spinlock__one_thread_double_lock_try' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12261:1-12272:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_spinlock__one_thread_locked_at_exit' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12285:1-12296:1)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_urb__less_initial_decrement' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12298:1-12309:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_update_lock_sched__more_unlocks' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12323:1-12334:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_update_lock_sched__locked_at_read_section' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12335:1-12346:1)
[Warning][Deadcode] Function '__blk_end_request' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12360:1-12362:1)
[Warning][Deadcode] Function '__blk_end_request_all' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12363:1-12365:1)
[Warning][Deadcode] Function '__blk_end_request_cur' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12367:1-12369:1)
[Warning][Deadcode] Function '__dynamic_dev_dbg' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12370:1-12372:1)
[Warning][Deadcode] Function 'add_disk' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12382:1-12384:1)
[Warning][Deadcode] Function 'alloc_disk' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12385:1-12387:1)
[Warning][Deadcode] Function 'blk_cleanup_queue' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12388:1-12390:1)
[Warning][Deadcode] Function 'blk_dump_rq_flags' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12391:1-12393:1)
[Warning][Deadcode] Function 'blk_fetch_request' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12394:1-12396:1)
[Warning][Deadcode] Function 'blk_init_queue' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12397:1-12399:1)
[Warning][Deadcode] Function 'blk_queue_bounce_limit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12400:1-12402:1)
[Warning][Deadcode] Function 'blk_queue_logical_block_size' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12403:1-12405:1)
[Warning][Deadcode] Function 'blk_queue_max_hw_sectors' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12406:1-12408:1)
[Warning][Deadcode] Function 'blk_queue_max_segment_size' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12409:1-12411:1)
[Warning][Deadcode] Function 'blk_queue_max_segments' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12412:1-12414:1)
[Warning][Deadcode] Function 'blk_queue_prep_rq' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12415:1-12417:1)
[Warning][Deadcode] Function 'blk_rq_map_sg' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12419:1-12421:1)
[Warning][Deadcode] Function 'complete_all' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12428:1-12430:1)
[Warning][Deadcode] Function 'del_gendisk' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12431:1-12433:1)
[Warning][Deadcode] Function 'ldv_assert' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12437:1-12439:1)
[Warning][Deadcode] Function 'memstick_init_req_sg' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12443:1-12445:1)
[Warning][Deadcode] Function 'put_disk' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12467:1-12469:1)
[Warning][Deadcode] Function 'scnprintf' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12475:1-12477:1)
[Warning][Deadcode] Function 'sg_init_one' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12478:1-12480:1)
[Warning][Deadcode] Function 'wait_for_completion' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12484:1-12486:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'ldv_EMGentry_exit_mspro_block_exit_3_2' has dead code:
  on line 7012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7012-7012)
[Warning][Deadcode] Function 'ldv_assert_linux_alloc_irq__wrong_flags' has dead code:
  on line 12031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12031-12031)
[Warning][Deadcode] Function 'ldv_assert_linux_arch_io__more_initial_at_exit' has dead code:
  on line 12203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12203-12203)
[Warning][Deadcode] Function 'ldv_assert_linux_block_genhd__delete_before_add' has dead code:
  on line 12158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12158-12158)
[Warning][Deadcode] Function 'ldv_assert_linux_block_genhd__more_initial_at_exit' has dead code:
  on line 12178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12178-12178)
[Warning][Deadcode] Function 'ldv_assert_linux_block_queue__more_initial_at_exit' has dead code:
  on line 12117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12117-12117)
[Warning][Deadcode] Function 'ldv_assert_linux_block_request__get_at_exit' has dead code:
  on line 12018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12018-12018)
[Warning][Deadcode] Function 'ldv_assert_linux_drivers_base_class__registered_at_exit' has dead code:
  on line 12080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12080-12080)
[Warning][Deadcode] Function 'ldv_assert_linux_fs_char_dev__registered_at_exit' has dead code:
  on line 11500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11500-11500)
[Warning][Deadcode] Function 'ldv_assert_linux_fs_sysfs__more_initial_at_exit' has dead code:
  on line 12241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12241-12241)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_mutex__one_thread_double_lock' has dead code:
  on line 11835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11835-11835)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_mutex__one_thread_double_unlock' has dead code:
  on line 11859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11859-11859)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_rwlock__read_lock_at_exit' has dead code:
  on line 11340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11340-11340)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_rwlock__write_lock_at_exit' has dead code:
  on line 11376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11376-11376)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_spinlock__one_thread_double_lock' has dead code:
  on line 12254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12254-12254)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_locking_spinlock__one_thread_double_unlock' has dead code:
  on line 12278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12278-12278)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_module__more_initial_at_exit' has dead code:
  on line 11562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11562-11562)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_srcu__locked_at_exit' has dead code:
  on line 11537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11537-11537)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_update_lock__locked_at_exit' has dead code:
  on line 11711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11711-11711)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_update_lock_bh__locked_at_exit' has dead code:
  on line 11773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11773-11773)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_update_lock_sched__locked_at_exit' has dead code:
  on line 12352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12352-12352)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_sched_completion__wait_without_init' has dead code:
  on line 11454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11454-11454)
[Warning][Deadcode] Function 'ldv_assert_linux_lib_idr__more_at_exit' has dead code:
  on line 11425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11425-11425)
[Warning][Deadcode] Function 'ldv_assert_linux_lib_idr__not_initialized' has dead code:
  on line 11405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11405-11405)
[Warning][Deadcode] Function 'ldv_assert_linux_mmc_sdio_func__unreleased_at_exit' has dead code:
  on line 11649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11649-11649)
[Warning][Deadcode] Function 'ldv_assert_linux_net_rtnetlink__lock_on_exit' has dead code:
  on line 11291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11291-11291)
[Warning][Deadcode] Function 'ldv_assert_linux_net_sock__all_locked_sockets_must_be_released' has dead code:
  on line 11724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11724-11724)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_coherent__more_initial_at_exit' has dead code:
  on line 11674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11674-11674)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_gadget__usb_gadget_registered_at_exit' has dead code:
  on line 11956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11956-11956)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_urb__more_initial_at_exit' has dead code:
  on line 12315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12315-12315)
[Warning][Deadcode] Function 'ldv_del_gendisk_128' has dead code:
  on line 7695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7695-7695)
  on line 7697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7697-7697)
[Warning][Deadcode] Function 'ldv_device_driver_io_instance_0' has dead code:
  on line 7071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7071-7071)
  on line 7117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7117-7117)
  on line 7183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7183-7183)
[Warning][Deadcode] Function 'ldv_entry_EMGentry_3' has dead code:
  on line 7224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7224-7224)
  on lines 7229..7230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7229-7230)
  on line 7232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7232-7232)
  on line 7234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7234-7234)
[Warning][Deadcode] Function 'ldv_idr_destroy_141' has dead code:
  on line 7806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7806-7806)
[Warning][Deadcode] Function 'ldv_idr_remove_98' has dead code:
  on line 7421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7421-7421)
[Warning][Deadcode] Function 'ldv_io_instance_release_0_19' has dead code:
  on line 7303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7303-7303)
[Warning][Deadcode] Function 'ldv_linux_alloc_irq_check_alloc_flags' has dead code:
  on line 7898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7898-7898)
[Warning][Deadcode] Function 'ldv_linux_alloc_usb_lock_check_alloc_flags' has dead code:
  on line 7960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7960-7960)
[Warning][Deadcode] Function 'ldv_linux_block_genhd_del_gendisk' has dead code:
  on line 8188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8188-8188)
  on line 8190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:8190-8190)
[Warning][Deadcode] Function 'ldv_linux_kernel_sched_completion_wait_for_completion_mrq_complete_of_memstick_dev' has dead code:
  on line 11189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11189-11189)
  on line 11191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11191-11191)
[Warning][Deadcode] Function 'ldv_linux_lib_idr_idr_destroy_mspro_block_disk_idr' has dead code:
  on lines 11247..11248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11247-11248)
  on line 11250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11250-11250)
[Warning][Deadcode] Function 'ldv_linux_lib_idr_idr_remove_mspro_block_disk_idr' has dead code:
  on lines 11236..11237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11236-11237)
  on line 11239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11239-11239)
[Warning][Deadcode] Function 'ldv_memstick_register_driver' has dead code:
  on line 7337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7337-7337)
[Warning][Deadcode] Function 'ldv_memstick_register_driver_139' has dead code:
  on line 7787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7787-7787)
[Warning][Deadcode] Function 'ldv_memstick_unregister_driver' has dead code:
  on line 7349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7349-7349)
[Warning][Deadcode] Function 'ldv_wait_for_completion_108' has dead code:
  on line 7498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7498-7498)
  on line 7500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7500-7500)
[Warning][Deadcode] Function 'main' has dead code:
  on line 7244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7244-7244)
[Warning][Deadcode] Function 'mspro_block_data_clear' has dead code:
  on line 6704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6704-6704)
  on lines 6708..6711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6708-6711)
  on line 6714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6714-6714)
  on line 6719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6719-6719)
[Warning][Deadcode] Function 'mspro_block_disk_release' has dead code:
  on line 4920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:4920-4920)
[Warning][Deadcode] Function 'mspro_block_exit' has dead code:
  on line 6980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6980-6980)
[Warning][Deadcode] Function 'mspro_block_init_card' has dead code:
  on lines 6470..6471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6470-6471)
  on line 6475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6475-6475)
  on lines 6477..6478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6477-6478)
  on lines 6482..6488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6482-6488)
  on line 6490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6490-6490)
  on line 6492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6492-6492)
  on lines 6496..6497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6496-6497)
  on lines 6501..6505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6501-6505)
  on lines 6507..6508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6507-6508)
  on lines 6512..6518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6512-6518)
  on line 6520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6520-6520)
  on line 6522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6522-6522)
  on lines 6528..6529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6528-6529)
  on lines 6531..6532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6531-6532)
  on lines 6536..6542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6536-6542)
  on line 6544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6544-6544)
  on line 6546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6546-6546)
  on line 6550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6550-6550)
[Warning][Deadcode] Function 'mspro_block_probe' has dead code:
  on line 6768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6768-6768)
  on line 6770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6770-6770)
  on line 6775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6775-6775)
  on lines 6777..6781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6777-6781)
  on line 6785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6785-6785)
[Warning][Deadcode] Function 'mspro_block_remove' has dead code:
  on lines 6812..6818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6812-6818)
  on line 6820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6820-6820)
  on line 6822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6822-6822)
  on lines 6827..6834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6827-6834)
  on line 6836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6836-6836)
[Warning][Deadcode] Function 'mspro_block_resume' has dead code:
  on line 6894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6894-6894)
  on lines 6898..6899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6898-6899)
  on line 6901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6901-6901)
  on line 6903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6903-6903)
  on line 6905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6905-6905)
  on line 6909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6909-6909)
  on line 6913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6913-6913)
  on line 6915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6915-6915)
[Warning][Deadcode] Function 'mspro_block_wait_for_ced' has dead code:
  on line 6052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6052-6052)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 628
  dead: 2184 (2031 in uncalled functions)
  total lines: 2812
[Warning][Deadcode][CWE-571] condition 'ldv_linux_lib_idr_idr_mspro_block_disk_idr == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11257:3-11257:141)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12029:7-12029:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11647:7-11647:13)
[Warning][Deadcode][CWE-571] condition 'major == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6956:7-6956:17)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11273:73-11273:74)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11672:7-11672:13)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7897:7-7897:10)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12078:7-12078:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11289:7-11289:13)
[Warning][Deadcode][CWE-571] condition 'rc != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6763:7-6763:14)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7903:3-7903:67)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11709:7-11709:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12115:7-12115:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11722:7-11722:13)
[Warning][Deadcode][CWE-571] condition '(unsigned long )data != (unsigned long )((struct ldv_struct_io_instance_0 *)0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7053:7-7053:85)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11338:7-11338:13)
[Warning][Deadcode][CWE-571] condition '! expr' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12152:7-12152:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11771:7-11771:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11374:7-11374:13)
[Warning][Deadcode][CWE-570] condition 'ldv_linux_alloc_usb_lock_lock == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:7958:7-7958:41)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12176:7-12176:13)
[Warning][Deadcode][CWE-571] condition '! expr' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11399:7-11399:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12201:7-12201:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11423:7-11423:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11833:7-11833:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12239:7-12239:13)
[Warning][Deadcode][CWE-571] condition '! expr' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11448:7-11448:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12252:7-12252:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11857:7-11857:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12276:7-12276:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11498:7-11498:13)
[Warning][Deadcode][CWE-571] condition 'tmp___1 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6890:7-6890:19)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12313:7-12313:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11535:7-11535:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12350:7-12350:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11954:7-11954:13)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:11560:7-11560:13)
[Warning][Deadcode][CWE-570] condition '(unsigned long )msb->attr_group.attrs != (unsigned long )((struct attribute **)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:6703:7-6703:88)
[Warning][Deadcode][CWE-570] condition '! expr' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko.cil.i:12016:7-12016:13)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
