./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---kernel--locking--locktorture.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---kernel--locking--locktorture.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---kernel--locking--locktorture.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] function torture_lock_busted_write_delay uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __const_udelay
[Info]     torture_random
[Info]     __VERIFIER_nondet_ulong
[Info]   "up":
[Info] function torture_spin_lock_write_delay uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __udelay
[Info]     __const_udelay
[Info]     torture_random
[Info]     __VERIFIER_nondet_ulong
[Info]   "up":
[Info]     ldv_dummy_resourceless_instance_callback_2_9
[Info]     ldv_struct_noname_2_dummy_resourceless_instance_2
[Info]     ldv_dispatch_register_dummy_resourceless_instance_1_6_5
[Info]     ldv_entry_EMGentry_6
[Info]     ldv_dummy_resourceless_instance_callback_4_9
[Info]     ldv_struct_noname_2_dummy_resourceless_instance_4
[Info]     ldv_dispatch_register_dummy_resourceless_instance_1_6_5
[Info]     ldv_entry_EMGentry_6
[Info] function torture_rwlock_write_delay uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __udelay
[Info]     __const_udelay
[Info]     torture_random
[Info]     __VERIFIER_nondet_ulong
[Info]   "up":
[Info]     ldv_dummy_resourceless_instance_callback_0_9
[Info]     ldv_struct_noname_2_dummy_resourceless_instance_0
[Info]     ldv_dispatch_register_dummy_resourceless_instance_1_6_5
[Info]     ldv_entry_EMGentry_6
[Info]     ldv_dummy_resourceless_instance_callback_5_9
[Info]     ldv_struct_noname_2_dummy_resourceless_instance_5
[Info]     ldv_dispatch_register_dummy_resourceless_instance_1_6_5
[Info]     ldv_entry_EMGentry_6
[Info] function torture_rwlock_read_delay uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __udelay
[Info]     __const_udelay
[Info]     torture_random
[Info]     __VERIFIER_nondet_ulong
[Info]   "up":
[Info]     ldv_dummy_resourceless_instance_callback_0_3
[Info]     ldv_struct_noname_2_dummy_resourceless_instance_0
[Info]     ldv_dispatch_register_dummy_resourceless_instance_1_6_5
[Info]     ldv_entry_EMGentry_6
[Info]     ldv_dummy_resourceless_instance_callback_2_3
[Info]     ldv_struct_noname_2_dummy_resourceless_instance_2
[Info]     ldv_dispatch_register_dummy_resourceless_instance_1_6_5
[Info]     ldv_entry_EMGentry_6
[Info]     ldv_dummy_resourceless_instance_callback_3_3
[Info]     ldv_struct_noname_2_dummy_resourceless_instance_3
[Info]     ldv_dispatch_register_dummy_resourceless_instance_1_6_5
[Info]     ldv_entry_EMGentry_6
[Info]     ldv_dummy_resourceless_instance_callback_4_3
[Info]     ldv_struct_noname_2_dummy_resourceless_instance_4
[Info]     ldv_dispatch_register_dummy_resourceless_instance_1_6_5
[Info]     ldv_entry_EMGentry_6
[Info]     ldv_dummy_resourceless_instance_callback_5_3
[Info]     ldv_struct_noname_2_dummy_resourceless_instance_5
[Info]     ldv_dispatch_register_dummy_resourceless_instance_1_6_5
[Info]     ldv_entry_EMGentry_6
[Info] function torture_mutex_delay uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __const_udelay
[Info]     torture_random
[Info]     __VERIFIER_nondet_ulong
[Info]   "up":
[Info]     ldv_dummy_resourceless_instance_callback_3_9
[Info]     ldv_struct_noname_2_dummy_resourceless_instance_3
[Info]     ldv_dispatch_register_dummy_resourceless_instance_1_6_5
[Info]     ldv_entry_EMGentry_6
[Info] function torture_rwsem_write_delay uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __const_udelay
[Info]     torture_random
[Info]     __VERIFIER_nondet_ulong
[Info]   "up":
[Info]     ldv_dummy_resourceless_instance_callback_1_9
[Info]     ldv_struct_noname_2_dummy_resourceless_instance_1
[Info]     ldv_dispatch_register_dummy_resourceless_instance_1_6_5
[Info]     ldv_entry_EMGentry_6
[Info] function torture_rwsem_read_delay uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __const_udelay
[Info]     torture_random
[Info]     __VERIFIER_nondet_ulong
[Info]   "up":
[Info]     ldv_dummy_resourceless_instance_callback_1_3
[Info]     ldv_struct_noname_2_dummy_resourceless_instance_1
[Info]     ldv_dispatch_register_dummy_resourceless_instance_1_6_5
[Info]     ldv_entry_EMGentry_6
[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())) )
[Error][Imprecise][Unsound] Function definition missing for __bad_percpu_size
[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---kernel--locking--locktorture.ko.cil.i:5467:3-5467:100)
[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---kernel--locking--locktorture.ko.cil.i:4743:7-4743:81)
[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---kernel--locking--locktorture.ko.cil.i:4753:5-4753:46)
[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---kernel--locking--locktorture.ko.cil.i:3611:3-3611:88)
[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---kernel--locking--locktorture.ko.cil.i:3611:3-3611:88)
[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---kernel--locking--locktorture.ko.cil.i:3611:3-3611:88)
[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---kernel--locking--locktorture.ko.cil.i:3598:3-3598:40)
[Warning][Unknown] lval (& srcp)->bits 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---kernel--locking--locktorture.ko.cil.i:3598:3-3598:40)
[Warning][Unknown] lval (& srcp)->bits points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:22:136-22:139)
[Warning][Unknown] lval (& srcp)->bits 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---kernel--locking--locktorture.ko.cil.i:10209:10-10209:33)
[Warning][Unknown] lval (& srcp)->bits 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---kernel--locking--locktorture.ko.cil.i:10209:10-10209:33)
[Warning][Unknown] lval (& srcp)->bits 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---kernel--locking--locktorture.ko.cil.i:3600:11-3600:19)
[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---kernel--locking--locktorture.ko.cil.i:3613:11-3613:30)
[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---kernel--locking--locktorture.ko.cil.i:4754:5-4754:51)
[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---kernel--locking--locktorture.ko.cil.i:4754:5-4754:51)
[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---kernel--locking--locktorture.ko.cil.i:4780:3-4780:74)
[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---kernel--locking--locktorture.ko.cil.i:4780:3-4780:74)
[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---kernel--locking--locktorture.ko.cil.i:4805:7-4805:84)
[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---kernel--locking--locktorture.ko.cil.i:4811:9-4811:50)
[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---kernel--locking--locktorture.ko.cil.i:4812:9-4812:48)
[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---kernel--locking--locktorture.ko.cil.i:4820:5-4820:76)
[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---kernel--locking--locktorture.ko.cil.i:4820:5-4820:76)
[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---kernel--locking--locktorture.ko.cil.i:4894:3-4894:73)
[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---kernel--locking--locktorture.ko.cil.i:4894:3-4894:73)
[Info][Unsound] Unknown value in {&(alloc@sid:707)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:7977:5-7977:44)
[Info][Unsound] Unknown value in {&(alloc@sid:707)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:7351:3-7351:23)
[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---kernel--locking--locktorture.ko.cil.i:4908:7-4908:84)
[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---kernel--locking--locktorture.ko.cil.i:4910:5-4910:76)
[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---kernel--locking--locktorture.ko.cil.i:4910:5-4910:76)
[Info][Unsound] Unknown value in {&(alloc@sid:718)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:7977:5-7977:44)
[Info][Unsound] Unknown value in {&(alloc@sid:718)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:7351:3-7351:23)
[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---kernel--locking--locktorture.ko.cil.i:4945:7-4945:116)
[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---kernel--locking--locktorture.ko.cil.i:4950:3-4953:71)
[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---kernel--locking--locktorture.ko.cil.i:4960:3-4960:12)
[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---kernel--locking--locktorture.ko.cil.i:4961:3-4961:12)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4492:3-4492:46)
[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---kernel--locking--locktorture.ko.cil.i:4492:3-4492:46)
[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---kernel--locking--locktorture.ko.cil.i:4493:7-4493:84)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4494:5-4494:57)
[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---kernel--locking--locktorture.ko.cil.i:4494:5-4494:57)
[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---kernel--locking--locktorture.ko.cil.i:4498:3-4498:37)
[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---kernel--locking--locktorture.ko.cil.i:4445:3-4445:31)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4455:3-4455:71)
[Info][Imprecise] Invalidating expressions: page (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4471:3-4473:57)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4471:3-4473:57)
[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---kernel--locking--locktorture.ko.cil.i:4474:3-4474:36)
[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---kernel--locking--locktorture.ko.cil.i:4474:3-4474: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---kernel--locking--locktorture.ko.cil.i:4513:7-4513:84)
[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---kernel--locking--locktorture.ko.cil.i:4515:5-4515:43)
[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---kernel--locking--locktorture.ko.cil.i:5594:3-5594:123)
[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---kernel--locking--locktorture.ko.cil.i:5145:3-5145: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---kernel--locking--locktorture.ko.cil.i:3919:3-3919:33)
[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---kernel--locking--locktorture.ko.cil.i:3921:7-3921:76)
[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---kernel--locking--locktorture.ko.cil.i:3921:7-3921:76)
[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---kernel--locking--locktorture.ko.cil.i:3930:5-3930:22)
[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---kernel--locking--locktorture.ko.cil.i:5585:3-5585:72)
[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---kernel--locking--locktorture.ko.cil.i:6931:3-6931:84)
[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---kernel--locking--locktorture.ko.cil.i:3982:4-3982:31)
[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---kernel--locking--locktorture.ko.cil.i:5577:3-5577:74)
[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---kernel--locking--locktorture.ko.cil.i:5570:3-5570:124)
[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---kernel--locking--locktorture.ko.cil.i:5173:3-5173: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---kernel--locking--locktorture.ko.cil.i:3866:3-3866:33)
[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---kernel--locking--locktorture.ko.cil.i:3868:7-3868:76)
[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---kernel--locking--locktorture.ko.cil.i:3868:7-3868:76)
[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---kernel--locking--locktorture.ko.cil.i:3877:5-3877:22)
[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---kernel--locking--locktorture.ko.cil.i:5564:3-5564:74)
[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---kernel--locking--locktorture.ko.cil.i:5559:3-5559:76)
[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---kernel--locking--locktorture.ko.cil.i:5697:3-5697:123)
[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---kernel--locking--locktorture.ko.cil.i:5201:3-5201: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---kernel--locking--locktorture.ko.cil.i:4158:3-4158:33)
[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---kernel--locking--locktorture.ko.cil.i:4160:7-4160:76)
[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---kernel--locking--locktorture.ko.cil.i:4160:7-4160:76)
[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---kernel--locking--locktorture.ko.cil.i:4169:5-4169:22)
[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---kernel--locking--locktorture.ko.cil.i:4183:5-4183:30)
[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---kernel--locking--locktorture.ko.cil.i:5688:3-5688:72)
[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---kernel--locking--locktorture.ko.cil.i:5680:3-5680:74)
[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---kernel--locking--locktorture.ko.cil.i:5673:3-5673:124)
[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---kernel--locking--locktorture.ko.cil.i:5229:3-5229: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---kernel--locking--locktorture.ko.cil.i:4095:3-4095:33)
[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---kernel--locking--locktorture.ko.cil.i:4097:7-4097:76)
[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---kernel--locking--locktorture.ko.cil.i:4097:7-4097:76)
[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---kernel--locking--locktorture.ko.cil.i:4106:5-4106:22)
[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---kernel--locking--locktorture.ko.cil.i:4120:5-4120:30)
[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---kernel--locking--locktorture.ko.cil.i:5667:3-5667:74)
[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---kernel--locking--locktorture.ko.cil.i:5662:3-5662:76)
[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---kernel--locking--locktorture.ko.cil.i:5800:3-5800:123)
[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---kernel--locking--locktorture.ko.cil.i:5257:3-5257: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---kernel--locking--locktorture.ko.cil.i:5791:3-5791:72)
[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---kernel--locking--locktorture.ko.cil.i:5783:3-5783:74)
[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---kernel--locking--locktorture.ko.cil.i:6465:3-6465:30)
[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---kernel--locking--locktorture.ko.cil.i:5776:3-5776:124)
[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---kernel--locking--locktorture.ko.cil.i:5285:3-5285:38)
[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---kernel--locking--locktorture.ko.cil.i:3779:3-3779:33)
[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---kernel--locking--locktorture.ko.cil.i:3781:7-3781:76)
[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---kernel--locking--locktorture.ko.cil.i:3781:7-3781:76)
[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---kernel--locking--locktorture.ko.cil.i:3790:5-3790:22)
[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---kernel--locking--locktorture.ko.cil.i:3798:3-3798:33)
[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---kernel--locking--locktorture.ko.cil.i:3800:7-3800:71)
[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---kernel--locking--locktorture.ko.cil.i:3800:7-3800:71)
[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---kernel--locking--locktorture.ko.cil.i:5770:3-5770:74)
[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---kernel--locking--locktorture.ko.cil.i:3962:4-3962:31)
[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---kernel--locking--locktorture.ko.cil.i:5765:3-5765:76)
[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---kernel--locking--locktorture.ko.cil.i:5903:3-5903:123)
[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---kernel--locking--locktorture.ko.cil.i:5313:3-5313: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---kernel--locking--locktorture.ko.cil.i:5894:3-5894:72)
[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---kernel--locking--locktorture.ko.cil.i:5886:3-5886:74)
[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---kernel--locking--locktorture.ko.cil.i:5879:3-5879:124)
[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---kernel--locking--locktorture.ko.cil.i:5341:3-5341:28)
[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---kernel--locking--locktorture.ko.cil.i:4024:3-4024:33)
[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---kernel--locking--locktorture.ko.cil.i:4026:7-4026:76)
[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---kernel--locking--locktorture.ko.cil.i:4026:7-4026:76)
[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---kernel--locking--locktorture.ko.cil.i:4035:5-4035:22)
[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---kernel--locking--locktorture.ko.cil.i:4049:5-4049:30)
[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---kernel--locking--locktorture.ko.cil.i:5873:3-5873:74)
[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---kernel--locking--locktorture.ko.cil.i:5868:3-5868:76)
[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---kernel--locking--locktorture.ko.cil.i:6006:3-6006:123)
[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---kernel--locking--locktorture.ko.cil.i:5369:3-5369: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---kernel--locking--locktorture.ko.cil.i:5997:3-5997:72)
[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---kernel--locking--locktorture.ko.cil.i:5989:3-5989:74)
[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---kernel--locking--locktorture.ko.cil.i:5982:3-5982:124)
[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---kernel--locking--locktorture.ko.cil.i:5397:3-5397:38)
[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---kernel--locking--locktorture.ko.cil.i:5976:3-5976:74)
[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---kernel--locking--locktorture.ko.cil.i:3636:3-3636:51)
[Info][Unsound] Unknown value in {&torture_spinlock.__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---kernel--locking--locktorture.ko.cil.i:3636:3-3636:51)
[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---kernel--locking--locktorture.ko.cil.i:10221:3-10221: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---kernel--locking--locktorture.ko.cil.i:5971:3-5971:76)
[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---kernel--locking--locktorture.ko.cil.i:3646:3-3646:53)
[Info][Unsound] Unknown value in {&torture_spinlock.__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---kernel--locking--locktorture.ko.cil.i:3646:3-3646:53)
[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---kernel--locking--locktorture.ko.cil.i:10224:3-10224: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---kernel--locking--locktorture.ko.cil.i:6109:3-6109:123)
[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---kernel--locking--locktorture.ko.cil.i:5425:3-5425: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---kernel--locking--locktorture.ko.cil.i:6100:3-6100:72)
[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---kernel--locking--locktorture.ko.cil.i:6092:3-6092:74)
[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---kernel--locking--locktorture.ko.cil.i:6085:3-6085:124)
[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---kernel--locking--locktorture.ko.cil.i:5453:3-5453: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---kernel--locking--locktorture.ko.cil.i:6079:3-6079:74)
[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---kernel--locking--locktorture.ko.cil.i:3828:4-3828:31)
[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---kernel--locking--locktorture.ko.cil.i:6074:3-6074:76)
[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---kernel--locking--locktorture.ko.cil.i:3837:3-3837:74)
[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---kernel--locking--locktorture.ko.cil.i:3656:3-3656:71)
[Info][Unsound] Unknown value in {&torture_spinlock.__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---kernel--locking--locktorture.ko.cil.i:3656:3-3656:71)
[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---kernel--locking--locktorture.ko.cil.i:10227:3-10227: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---kernel--locking--locktorture.ko.cil.i:5491:5-5491:88)
[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---kernel--locking--locktorture.ko.cil.i:3458:1-3467: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---kernel--locking--locktorture.ko.cil.i:3478:1-3489: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---kernel--locking--locktorture.ko.cil.i:3491:1-3507: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---kernel--locking--locktorture.ko.cil.i:3508:1-3524:1)
[Warning][Deadcode] Function 'get_current' is uncalled: 19 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:3546:1-3589:1)
[Warning][Deadcode] Function 'torture_lock_busted_write_lock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:3710:1-3715:1)
[Warning][Deadcode] Function 'torture_lock_busted_write_delay' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:3716:1-3745:1)
[Warning][Deadcode] Function 'torture_lock_busted_write_unlock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:3746:1-3751:1)
[Warning][Deadcode] Function 'torture_rwlock_read_lock' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:3899:1-3907:1)
[Warning][Deadcode] Function 'torture_rwlock_read_unlock' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:3943:1-3951:1)
[Warning][Deadcode] Function 'lock_torture_writer' is uncalled: 51 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4205:1-4337:1)
[Warning][Deadcode] Function 'lock_torture_reader' is uncalled: 38 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4338:1-4432:1)
[Warning][Deadcode] Function 'lock_torture_stats' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4535:1-4567: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---kernel--locking--locktorture.ko.cil.i:6317:1-6332: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---kernel--locking--locktorture.ko.cil.i:6336:1-6349: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---kernel--locking--locktorture.ko.cil.i:6350:1-6360: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---kernel--locking--locktorture.ko.cil.i:6376:1-6384: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---kernel--locking--locktorture.ko.cil.i:6385:1-6391: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---kernel--locking--locktorture.ko.cil.i:6392:1-6410: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---kernel--locking--locktorture.ko.cil.i:6411:1-6429: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---kernel--locking--locktorture.ko.cil.i:6430:1-6436: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---kernel--locking--locktorture.ko.cil.i:6437:1-6443: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---kernel--locking--locktorture.ko.cil.i:6444:1-6450: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---kernel--locking--locktorture.ko.cil.i:6451:1-6461: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---kernel--locking--locktorture.ko.cil.i:6469:1-6475: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---kernel--locking--locktorture.ko.cil.i:6476:1-6486: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---kernel--locking--locktorture.ko.cil.i:6487:1-6497: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---kernel--locking--locktorture.ko.cil.i:6498:1-6504: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---kernel--locking--locktorture.ko.cil.i:6505:1-6511: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---kernel--locking--locktorture.ko.cil.i:6512:1-6518: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---kernel--locking--locktorture.ko.cil.i:6522:1-6538: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---kernel--locking--locktorture.ko.cil.i:6539:1-6548: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---kernel--locking--locktorture.ko.cil.i:6564:1-6573:1)
[Warning][Deadcode] Function 'ldv_linux_block_genhd_del_gendisk' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:6574:1-6583: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---kernel--locking--locktorture.ko.cil.i:6584:1-6596: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---kernel--locking--locktorture.ko.cil.i:6610:1-6619: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---kernel--locking--locktorture.ko.cil.i:6634:1-6643: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---kernel--locking--locktorture.ko.cil.i:6658:1-6677: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---kernel--locking--locktorture.ko.cil.i:6678:1-6694: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---kernel--locking--locktorture.ko.cil.i:6695:1-6704: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---kernel--locking--locktorture.ko.cil.i:6705:1-6725: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---kernel--locking--locktorture.ko.cil.i:6736:1-6745: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---kernel--locking--locktorture.ko.cil.i:6746:1-6757: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---kernel--locking--locktorture.ko.cil.i:6758:1-6776: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---kernel--locking--locktorture.ko.cil.i:6783:1-6788: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---kernel--locking--locktorture.ko.cil.i:6789:1-6794: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---kernel--locking--locktorture.ko.cil.i:6795:1-6814: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---kernel--locking--locktorture.ko.cil.i:6819:1-6842: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---kernel--locking--locktorture.ko.cil.i:6843:1-6859: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---kernel--locking--locktorture.ko.cil.i:6860:1-6869: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---kernel--locking--locktorture.ko.cil.i:6882:1-6898: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---kernel--locking--locktorture.ko.cil.i:6899:1-6908: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---kernel--locking--locktorture.ko.cil.i:6936:1-6945: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---kernel--locking--locktorture.ko.cil.i:6966:1-6984: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---kernel--locking--locktorture.ko.cil.i:6985:1-7003: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---kernel--locking--locktorture.ko.cil.i:7017:1-7026: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---kernel--locking--locktorture.ko.cil.i:7027:1-7045: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---kernel--locking--locktorture.ko.cil.i:7046:1-7058: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---kernel--locking--locktorture.ko.cil.i:7059:1-7068: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---kernel--locking--locktorture.ko.cil.i:7069:1-7074: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---kernel--locking--locktorture.ko.cil.i:7088:1-7094: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---kernel--locking--locktorture.ko.cil.i:7095:1-7104: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---kernel--locking--locktorture.ko.cil.i:7105:1-7113: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---kernel--locking--locktorture.ko.cil.i:7127:1-7133: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---kernel--locking--locktorture.ko.cil.i:7134:1-7143: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---kernel--locking--locktorture.ko.cil.i:7144:1-7152: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---kernel--locking--locktorture.ko.cil.i:7166:1-7172: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---kernel--locking--locktorture.ko.cil.i:7173:1-7182: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---kernel--locking--locktorture.ko.cil.i:7183:1-7191: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---kernel--locking--locktorture.ko.cil.i:7205:1-7211: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---kernel--locking--locktorture.ko.cil.i:7212:1-7221: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---kernel--locking--locktorture.ko.cil.i:7222:1-7230: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---kernel--locking--locktorture.ko.cil.i:7261:1-7270:1)
[Warning][Deadcode] Function 'ldv_filter_err_code' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:7271:1-7280: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---kernel--locking--locktorture.ko.cil.i:7284:1-7290: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---kernel--locking--locktorture.ko.cil.i:7291:1-7297: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---kernel--locking--locktorture.ko.cil.i:7306:1-7320: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---kernel--locking--locktorture.ko.cil.i:7321:1-7334: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---kernel--locking--locktorture.ko.cil.i:7361:1-7369: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---kernel--locking--locktorture.ko.cil.i:7370:1-7379: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---kernel--locking--locktorture.ko.cil.i:7380:1-7389: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---kernel--locking--locktorture.ko.cil.i:7402:1-7418: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---kernel--locking--locktorture.ko.cil.i:7426:1-7440: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---kernel--locking--locktorture.ko.cil.i:7445:1-7454: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---kernel--locking--locktorture.ko.cil.i:7455:1-7464: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---kernel--locking--locktorture.ko.cil.i:7465:1-7474: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---kernel--locking--locktorture.ko.cil.i:7475:1-7492: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---kernel--locking--locktorture.ko.cil.i:7493:1-7508: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---kernel--locking--locktorture.ko.cil.i:7521:1-7527: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---kernel--locking--locktorture.ko.cil.i:7528:1-7542: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---kernel--locking--locktorture.ko.cil.i:7543:1-7552: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---kernel--locking--locktorture.ko.cil.i:7553:1-7562: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---kernel--locking--locktorture.ko.cil.i:7575:1-7591: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---kernel--locking--locktorture.ko.cil.i:7592:1-7604: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---kernel--locking--locktorture.ko.cil.i:7619:1-7628: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---kernel--locking--locktorture.ko.cil.i:7629:1-7646: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---kernel--locking--locktorture.ko.cil.i:7647:1-7658: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---kernel--locking--locktorture.ko.cil.i:7659:1-7665: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---kernel--locking--locktorture.ko.cil.i:7666:1-7674: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---kernel--locking--locktorture.ko.cil.i:7683:1-7699: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---kernel--locking--locktorture.ko.cil.i:7700:1-7715: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---kernel--locking--locktorture.ko.cil.i:7716:1-7724: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---kernel--locking--locktorture.ko.cil.i:7725:1-7745: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---kernel--locking--locktorture.ko.cil.i:7746:1-7768: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---kernel--locking--locktorture.ko.cil.i:7769:1-7784: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---kernel--locking--locktorture.ko.cil.i:7785:1-7793: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---kernel--locking--locktorture.ko.cil.i:7794:1-7810: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---kernel--locking--locktorture.ko.cil.i:7811:1-7820: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---kernel--locking--locktorture.ko.cil.i:7833:1-7849: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---kernel--locking--locktorture.ko.cil.i:7857:1-7871: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---kernel--locking--locktorture.ko.cil.i:7875:1-7887: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---kernel--locking--locktorture.ko.cil.i:7917:1-7922: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---kernel--locking--locktorture.ko.cil.i:7923:1-7931:1)
[Warning][Deadcode] Function 'ldv_free' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:7996:1-8004: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---kernel--locking--locktorture.ko.cil.i:8021:1-8036: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---kernel--locking--locktorture.ko.cil.i:8050:1-8059: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---kernel--locking--locktorture.ko.cil.i:8060:1-8072: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---kernel--locking--locktorture.ko.cil.i:8073:1-8085: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---kernel--locking--locktorture.ko.cil.i:8092:1-8104: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---kernel--locking--locktorture.ko.cil.i:8105:1-8127: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---kernel--locking--locktorture.ko.cil.i:8128:1-8133: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---kernel--locking--locktorture.ko.cil.i:8134:1-8139: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---kernel--locking--locktorture.ko.cil.i:8145:1-8154: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---kernel--locking--locktorture.ko.cil.i:8155:1-8170: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---kernel--locking--locktorture.ko.cil.i:8171:1-8188: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---kernel--locking--locktorture.ko.cil.i:8189:1-8204: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---kernel--locking--locktorture.ko.cil.i:8205:1-8219: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---kernel--locking--locktorture.ko.cil.i:8220:1-8229:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_lock_interruptible_or_killable_torture_mutex' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8241:1-8256:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_is_locked_torture_mutex' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8257:1-8274:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_mutex_trylock_torture_mutex' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8275:1-8290:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_atomic_dec_and_mutex_lock_torture_mutex' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8291:1-8305:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_initialize' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8316:1-8323:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_mutex_check_final_state' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8324:1-8333: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---kernel--locking--locktorture.ko.cil.i:8339:1-8349: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---kernel--locking--locktorture.ko.cil.i:8350:1-8360: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---kernel--locking--locktorture.ko.cil.i:8361:1-8377: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---kernel--locking--locktorture.ko.cil.i:8378:1-8387: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---kernel--locking--locktorture.ko.cil.i:8388:1-8401: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---kernel--locking--locktorture.ko.cil.i:8402:1-8411: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---kernel--locking--locktorture.ko.cil.i:8412:1-8425: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---kernel--locking--locktorture.ko.cil.i:8426:1-8442: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---kernel--locking--locktorture.ko.cil.i:8444:1-8454: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---kernel--locking--locktorture.ko.cil.i:8455:1-8465: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---kernel--locking--locktorture.ko.cil.i:8466:1-8482: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---kernel--locking--locktorture.ko.cil.i:8483:1-8492: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---kernel--locking--locktorture.ko.cil.i:8493:1-8506: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---kernel--locking--locktorture.ko.cil.i:8507:1-8516: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---kernel--locking--locktorture.ko.cil.i:8517:1-8530: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---kernel--locking--locktorture.ko.cil.i:8531:1-8547: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---kernel--locking--locktorture.ko.cil.i:8549:1-8559: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---kernel--locking--locktorture.ko.cil.i:8560:1-8570: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---kernel--locking--locktorture.ko.cil.i:8571:1-8587: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---kernel--locking--locktorture.ko.cil.i:8588:1-8597: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---kernel--locking--locktorture.ko.cil.i:8598:1-8611: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---kernel--locking--locktorture.ko.cil.i:8612:1-8621: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---kernel--locking--locktorture.ko.cil.i:8622:1-8635: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---kernel--locking--locktorture.ko.cil.i:8636:1-8652: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---kernel--locking--locktorture.ko.cil.i:8654:1-8664: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---kernel--locking--locktorture.ko.cil.i:8665:1-8675: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---kernel--locking--locktorture.ko.cil.i:8676:1-8692: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---kernel--locking--locktorture.ko.cil.i:8693:1-8702: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---kernel--locking--locktorture.ko.cil.i:8703:1-8716: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---kernel--locking--locktorture.ko.cil.i:8717:1-8726: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---kernel--locking--locktorture.ko.cil.i:8727:1-8740: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---kernel--locking--locktorture.ko.cil.i:8741:1-8757: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---kernel--locking--locktorture.ko.cil.i:8759:1-8769: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---kernel--locking--locktorture.ko.cil.i:8770:1-8780: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---kernel--locking--locktorture.ko.cil.i:8781:1-8797: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---kernel--locking--locktorture.ko.cil.i:8798:1-8807: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---kernel--locking--locktorture.ko.cil.i:8808:1-8821: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---kernel--locking--locktorture.ko.cil.i:8822:1-8831: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---kernel--locking--locktorture.ko.cil.i:8832:1-8845: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---kernel--locking--locktorture.ko.cil.i:8846:1-8862:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_trylock_torture_spinlock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8886:1-8902:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_unlock_wait_torture_spinlock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8903:1-8912:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_locked_torture_spinlock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8913:1-8926:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_can_lock_torture_spinlock' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8927:1-8936:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_spin_is_contended_torture_spinlock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8937:1-8950:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_atomic_dec_and_lock_torture_spinlock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8951:1-8967:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_locking_spinlock_check_final_state' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8968:1-8981:1)
[Warning][Deadcode] Function 'ldv_exclusive_spin_is_locked' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:8982:1-9011:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_sched_completion_init_completion' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9015:1-9021:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_sched_completion_init_completion_macro' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9022:1-9031:1)
[Warning][Deadcode] Function 'ldv_linux_kernel_sched_completion_wait_for_completion' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9032:1-9041:1)
[Warning][Deadcode] Function 'ldv_linux_lib_idr_idr_init' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9047:1-9056:1)
[Warning][Deadcode] Function 'ldv_linux_lib_idr_idr_alloc' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9057:1-9067:1)
[Warning][Deadcode] Function 'ldv_linux_lib_idr_idr_find' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9068:1-9078:1)
[Warning][Deadcode] Function 'ldv_linux_lib_idr_idr_remove' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9079:1-9089:1)
[Warning][Deadcode] Function 'ldv_linux_lib_idr_idr_destroy' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9090:1-9100: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---kernel--locking--locktorture.ko.cil.i:9122:1-9133: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---kernel--locking--locktorture.ko.cil.i:9146:1-9157: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---kernel--locking--locktorture.ko.cil.i:9171:1-9182: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---kernel--locking--locktorture.ko.cil.i:9232:1-9243:1)
[Warning][Deadcode] Function 'ldv_assert_linux_lib_idr__not_initialized' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9244:1-9255: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---kernel--locking--locktorture.ko.cil.i:9256:1-9267: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---kernel--locking--locktorture.ko.cil.i:9281:1-9292:1)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_sched_completion__wait_without_init' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9293:1-9304: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---kernel--locking--locktorture.ko.cil.i:9306:1-9317: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---kernel--locking--locktorture.ko.cil.i:9319:1-9330: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---kernel--locking--locktorture.ko.cil.i:9331:1-9342: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---kernel--locking--locktorture.ko.cil.i:9356:1-9367: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---kernel--locking--locktorture.ko.cil.i:9368:1-9379: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---kernel--locking--locktorture.ko.cil.i:9393:1-9404: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---kernel--locking--locktorture.ko.cil.i:9418:1-9429: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---kernel--locking--locktorture.ko.cil.i:9430:1-9441: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---kernel--locking--locktorture.ko.cil.i:9443:1-9454: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---kernel--locking--locktorture.ko.cil.i:9456:1-9467: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---kernel--locking--locktorture.ko.cil.i:9468:1-9479: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---kernel--locking--locktorture.ko.cil.i:9480:1-9491: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---kernel--locking--locktorture.ko.cil.i:9505:1-9516: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---kernel--locking--locktorture.ko.cil.i:9530:1-9541: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---kernel--locking--locktorture.ko.cil.i:9542:1-9553: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---kernel--locking--locktorture.ko.cil.i:9579:1-9590: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---kernel--locking--locktorture.ko.cil.i:9592:1-9603: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---kernel--locking--locktorture.ko.cil.i:9604:1-9615: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---kernel--locking--locktorture.ko.cil.i:9629:1-9640: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---kernel--locking--locktorture.ko.cil.i:9641:1-9652: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---kernel--locking--locktorture.ko.cil.i:9653:1-9664: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---kernel--locking--locktorture.ko.cil.i:9665:1-9676: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---kernel--locking--locktorture.ko.cil.i:9690:1-9701: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---kernel--locking--locktorture.ko.cil.i:9714:1-9725: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---kernel--locking--locktorture.ko.cil.i:9727:1-9738: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---kernel--locking--locktorture.ko.cil.i:9739:1-9750: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---kernel--locking--locktorture.ko.cil.i:9751:1-9762: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---kernel--locking--locktorture.ko.cil.i:9763:1-9774: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---kernel--locking--locktorture.ko.cil.i:9775:1-9786: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---kernel--locking--locktorture.ko.cil.i:9787:1-9798: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---kernel--locking--locktorture.ko.cil.i:9812:1-9823: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---kernel--locking--locktorture.ko.cil.i:9824:1-9835: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---kernel--locking--locktorture.ko.cil.i:9837:1-9848: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---kernel--locking--locktorture.ko.cil.i:9849:1-9860: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---kernel--locking--locktorture.ko.cil.i:9886:1-9897: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---kernel--locking--locktorture.ko.cil.i:9899:1-9910: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---kernel--locking--locktorture.ko.cil.i:9911:1-9922: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---kernel--locking--locktorture.ko.cil.i:9936:1-9947: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---kernel--locking--locktorture.ko.cil.i:9948:1-9959: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---kernel--locking--locktorture.ko.cil.i:9973:1-9984: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---kernel--locking--locktorture.ko.cil.i:9985:1-9996:1)
[Warning][Deadcode] Function 'ldv_assert_linux_block_genhd__delete_before_add' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9997:1-10008: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---kernel--locking--locktorture.ko.cil.i:10009:1-10020: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---kernel--locking--locktorture.ko.cil.i:10034:1-10045: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---kernel--locking--locktorture.ko.cil.i:10059:1-10070: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---kernel--locking--locktorture.ko.cil.i:10072:1-10083: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---kernel--locking--locktorture.ko.cil.i:10109:1-10120: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---kernel--locking--locktorture.ko.cil.i:10133:1-10144: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---kernel--locking--locktorture.ko.cil.i:10146:1-10157: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---kernel--locking--locktorture.ko.cil.i:10171:1-10182: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---kernel--locking--locktorture.ko.cil.i:10183:1-10194: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---kernel--locking--locktorture.ko.cil.i:10245:1-10247:1)
[Warning][Deadcode] Function 'schedule_timeout_interruptible' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10253:1-10255:1)
[Warning][Deadcode] Function 'schedule_timeout_uninterruptible' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10257:1-10259:1)
[Warning][Deadcode] Function 'set_user_nice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10260:1-10262:1)
[Warning][Deadcode] Function 'stutter_wait' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10263:1-10265:1)
[Warning][Deadcode] Function 'torture_kthread_stopping' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10280:1-10282:1)
[Warning][Deadcode] Function 'torture_must_stop' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10284:1-10286:1)
[Warning][Deadcode] Function 'torture_onoff_init' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10292:1-10294:1)
[Warning][Deadcode] Function 'torture_shutdown_absorb' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10303:1-10305:1)
[Warning][Deadcode] Function 'torture_shutdown_init' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10307:1-10309:1)
[Warning][Deadcode] Function 'warn_slowpath_null' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10320:1-10322:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'ldv_assert_linux_alloc_irq__wrong_flags' has dead code:
  on line 9879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9879-9879)
[Warning][Deadcode] Function 'ldv_assert_linux_arch_io__more_initial_at_exit' has dead code:
  on line 10051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10051-10051)
[Warning][Deadcode] Function 'ldv_assert_linux_block_genhd__more_initial_at_exit' has dead code:
  on line 10026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10026-10026)
[Warning][Deadcode] Function 'ldv_assert_linux_block_queue__more_initial_at_exit' has dead code:
  on line 9965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9965-9965)
[Warning][Deadcode] Function 'ldv_assert_linux_block_request__get_at_exit' has dead code:
  on line 9866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9866-9866)
[Warning][Deadcode] Function 'ldv_assert_linux_drivers_base_class__registered_at_exit' has dead code:
  on line 9928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9928-9928)
[Warning][Deadcode] Function 'ldv_assert_linux_fs_char_dev__registered_at_exit' has dead code:
  on line 9348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9348-9348)
[Warning][Deadcode] Function 'ldv_assert_linux_fs_sysfs__more_initial_at_exit' has dead code:
  on line 10089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10089-10089)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_module__more_initial_at_exit' has dead code:
  on line 9410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9410-9410)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_srcu__locked_at_exit' has dead code:
  on line 9385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9385-9385)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_update_lock__locked_at_exit' has dead code:
  on line 9559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9559-9559)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_update_lock_bh__locked_at_exit' has dead code:
  on line 9621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9621-9621)
[Warning][Deadcode] Function 'ldv_assert_linux_kernel_rcu_update_lock_sched__locked_at_exit' has dead code:
  on line 10200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10200-10200)
[Warning][Deadcode] Function 'ldv_assert_linux_lib_idr__more_at_exit' has dead code:
  on line 9273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9273-9273)
[Warning][Deadcode] Function 'ldv_assert_linux_mmc_sdio_func__unreleased_at_exit' has dead code:
  on line 9497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9497-9497)
[Warning][Deadcode] Function 'ldv_assert_linux_net_rtnetlink__lock_on_exit' has dead code:
  on line 9139 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9139-9139)
[Warning][Deadcode] Function 'ldv_assert_linux_net_sock__all_locked_sockets_must_be_released' has dead code:
  on line 9572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9572-9572)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_coherent__more_initial_at_exit' has dead code:
  on line 9522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9522-9522)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_gadget__usb_gadget_registered_at_exit' has dead code:
  on line 9804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9804-9804)
[Warning][Deadcode] Function 'ldv_assert_linux_usb_urb__more_initial_at_exit' has dead code:
  on line 10163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:10163-10163)
[Warning][Deadcode] Function 'ldv_entry_EMGentry_6' has dead code:
  on line 5477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5477-5477)
  on line 5495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5495-5495)
  on line 5497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5497-5497)
[Warning][Deadcode] Function 'ldv_linux_alloc_irq_check_alloc_flags' has dead code:
  on line 6307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:6307-6307)
[Warning][Deadcode] Function 'ldv_linux_alloc_usb_lock_check_alloc_flags' has dead code:
  on line 6369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:6369-6369)
[Warning][Deadcode] Function 'ldv_struct_noname_2_dummy_resourceless_instance_0' has dead code:
  on line 5522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5522-5522)
  on line 5610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5610-5610)
[Warning][Deadcode] Function 'ldv_struct_noname_2_dummy_resourceless_instance_1' has dead code:
  on line 5625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5625-5625)
  on line 5713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5713-5713)
[Warning][Deadcode] Function 'ldv_struct_noname_2_dummy_resourceless_instance_2' has dead code:
  on line 5728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5728-5728)
  on line 5816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5816-5816)
[Warning][Deadcode] Function 'ldv_struct_noname_2_dummy_resourceless_instance_3' has dead code:
  on line 5831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5831-5831)
  on line 5919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5919-5919)
[Warning][Deadcode] Function 'ldv_struct_noname_2_dummy_resourceless_instance_4' has dead code:
  on line 5934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5934-5934)
  on line 6022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:6022-6022)
[Warning][Deadcode] Function 'ldv_struct_noname_2_dummy_resourceless_instance_5' has dead code:
  on line 6037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:6037-6037)
  on line 6125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:6125-6125)
[Warning][Deadcode] Function 'lock_torture_init' has dead code:
  on line 4745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4745-4745)
  on line 4750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4750-4750)
  on line 4761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4761-4761)
  on line 4771 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4771-4771)
  on lines 4773..4774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4773-4774)
  on line 4807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4807-4807)
  on line 4855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4855-4855)
  on line 4857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4857-4857)
  on line 4875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4875-4875)
  on line 4877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4877-4877)
[Warning][Deadcode] Function 'main' has dead code:
  on line 5507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:5507-5507)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 1000
  dead: 1098 (1049 in uncalled functions)
  total lines: 2098
[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---kernel--locking--locktorture.ko.cil.i:9137:7-9137: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---kernel--locking--locktorture.ko.cil.i:9926:7-9926:13)
[Warning][Deadcode][CWE-571] condition '(int )verbose' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4914:11-4914:24)
[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---kernel--locking--locktorture.ko.cil.i:9963:7-9963: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---kernel--locking--locktorture.ko.cil.i:10024:7-10024:13)
[Warning][Deadcode][CWE-571] condition 'stat_interval > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4967:7-4967:24)
[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---kernel--locking--locktorture.ko.cil.i:10049:7-10049: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---kernel--locking--locktorture.ko.cil.i:9271:7-9271: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---kernel--locking--locktorture.ko.cil.i:10087:7-10087: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---kernel--locking--locktorture.ko.cil.i:9346:7-9346: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---kernel--locking--locktorture.ko.cil.i:10161:7-10161: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---kernel--locking--locktorture.ko.cil.i:9383:7-9383: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---kernel--locking--locktorture.ko.cil.i:9408:7-9408: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---kernel--locking--locktorture.ko.cil.i:10198:7-10198: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---kernel--locking--locktorture.ko.cil.i:9495:7-9495: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---kernel--locking--locktorture.ko.cil.i:9520:7-9520: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---kernel--locking--locktorture.ko.cil.i:6306:7-6306: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---kernel--locking--locktorture.ko.cil.i:9557:7-9557:13)
[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---kernel--locking--locktorture.ko.cil.i:6312:3-6312: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---kernel--locking--locktorture.ko.cil.i:9570:7-9570:13)
[Warning][Deadcode][CWE-570] condition '(unsigned long )(cxt.cur_ops)->init != (unsigned long )((void (*)(void))0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4743:7-4743:81)
[Warning][Deadcode][CWE-570] condition 'nwriters_stress >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4749:7-4749:27)
[Warning][Deadcode][CWE-570] condition 'tmp___3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4760:7-4760: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---kernel--locking--locktorture.ko.cil.i:9619:7-9619:13)
[Warning][Deadcode][CWE-571] condition 'tmp___4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4767:7-4767:19)
[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---kernel--locking--locktorture.ko.cil.i:6367:7-6367:41)
[Warning][Deadcode][CWE-571] condition '(int )verbose' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4784:9-4784:22)
[Warning][Deadcode][CWE-570] condition 'nreaders_stress >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4806:9-4806:29)
[Warning][Deadcode][CWE-571] condition 'nwriters_stress < 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4809:11-4809:30)
[Warning][Deadcode][CWE-571] condition '(int )verbose' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4824:11-4824:24)
[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---kernel--locking--locktorture.ko.cil.i:9802:7-9802:13)
[Warning][Deadcode][CWE-570] condition 'onoff_interval > 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4853:7-4853:25)
[Warning][Deadcode][CWE-571] condition 'shuffle_interval > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4863:7-4863:27)
[Warning][Deadcode][CWE-570] condition 'shutdown_secs > 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4873:7-4873:24)
[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---kernel--locking--locktorture.ko.cil.i:9864:7-9864:13)
[Warning][Deadcode][CWE-571] condition 'ldv_linux_lib_idr_idr == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:9105:3-9105:99)
[Warning][Deadcode][CWE-571] condition 'stutter > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4883:7-4883:18)
[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---kernel--locking--locktorture.ko.cil.i:9877:7-9877:13)
[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---kernel--locking--locktorture.ko.cil.i:9121:73-9121:74)
[Warning][Deadcode][CWE-571] condition '(int )verbose' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko.cil.i:4898:9-4898:22)
[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
[Error][Imprecise][Unsound] Function definition missing
