./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/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.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/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.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-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] 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 __xadd_wrong_size
[Error][Imprecise][Unsound] Function definition missing for __bad_percpu_size
[Error][Imprecise][Unsound] Function definition missing for __xchg_wrong_size
[Error][Imprecise][Unsound] Function definition missing for ldv_xmalloc
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4908:5-4908:49)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5030:7-5030:84)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4272:3-4272:32)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5099:3-5099:47)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5099:3-5099:47)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6388:3-6388:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5100:3-5100:28)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5100:3-5100:28)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6754:3-6754:9)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5101:3-5101:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4278:5-4278:44)
[Info][Imprecise] Invalidating expressions: tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4306:5-4306:55)
[Info][Imprecise] Invalidating expressions: & tmp___2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4306:5-4306:55)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4307:5-4307:40)
[Info][Imprecise] Invalidating expressions: tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4302:5-4302:57)
[Info][Imprecise] Invalidating expressions: & tmp___1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4302:5-4302:57)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4303:5-4303:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4326:3-4326:12)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4327:3-4327:34)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5107:3-5107:49)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5107:3-5107:49)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6446:3-6446:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5108:3-5108:30)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5108:3-5108:30)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6761:3-6761:9)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5109:3-5109:9)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4328:11-4328:43)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4328:11-4328:43)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5022:7-5023:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4366:3-4366:32)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5115:3-5115:47)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5115:3-5115:47)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5116:3-5116:28)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5116:3-5116:28)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5117:3-5117:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4371:5-4371:41)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4446:3-4446:20)
[Info][Unsound] Unknown address in {&data} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4456:3-4456:45)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4456:3-4456:45)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4485:5-4485:48)
[Warning][Imprecise][Call] Function pointer *(dev->change_protocol) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4485:5-4485:48)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4485:5-4485:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4509:5-4509:49)
[Warning][Unknown] lval (& dev)->rc_map.lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3313:11-3313:34)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4510:5-4510:44)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4511:5-4511:46)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4512:5-4512:54)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3333:3-3333:61)
[Warning][Unknown] lval (& dev)->rc_map.lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3333:3-3333:61)
[Warning][Unknown] lval (& dev)->rc_map.lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6655:3-6655:9)
[Warning][Unknown] lval (& lock)->ldv_5961.rlock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6655:3-6655:9)
[Warning][Unknown] lval (& dev)->rc_map.lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3334:3-3334:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4514:6-4514:41)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4531:3-4531:22)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4533:3-4533:34)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5123:3-5123:49)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5123:3-5123:49)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5124:3-5124:30)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5124:3-5124:30)
[Warning][Unknown] lval (& dev)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5125:3-5125:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5004:7-5004:35)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4232:3-4232:45)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3356:7-3356:75)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3357:13-3357:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3360:3-3360:34)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3360:3-3360:34)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3346:11-3346:36)
[Warning][Unknown] lval (& dev)->kobj points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3346:11-3346:36)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4233:3-4233:42)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3319:3-3319:41)
[Info][Unsound] Unknown value in {&rc_map_lock.ldv_5961.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3319:3-3319:41)
[Warning][Unknown] lval (& lock)->ldv_5961.rlock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6639:3-6639:9)
[Warning][Unknown] lval (& map)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3236:3-3236:36)
[Warning][Unknown] lval (& map)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6623:3-6623:9)
[Warning][Unknown] lval (& map)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3237:3-3237:9)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3326:3-3326:43)
[Info][Unsound] Unknown value in {&rc_map_lock.ldv_5961.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3326:3-3326:43)
[Warning][Unknown] lval (& lock)->ldv_5961.rlock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6649:3-6649:9)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4950:7-4950:28)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4936:7-4936:49)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4558:5-4558:59)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4567:5-4567:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4941:7-4941:49)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4928:7-4928:41)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4930:7-4930:28)
[Warning][Unknown] lval (& map)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6734:3-6734:9)
[Warning][Deadcode] Function 'set_bit' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3185:1-3191:1)
[Warning][Deadcode] Function '__set_bit' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3192:1-3198:1)
[Warning][Deadcode] Function '__clear_bit' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3199:1-3205:1)
[Warning][Deadcode] Function 'fls64' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3206:1-3213:1)
[Warning][Deadcode] Function 'fls_long' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3214:1-3220:1)
[Warning][Deadcode] Function '__roundup_pow_of_two' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3221:1-3227:1)
[Warning][Deadcode] Function 'atomic_add_return' is uncalled: 16 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3247:1-3274:1)
[Warning][Deadcode] Function 'input_allocate_device' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3372:1-3374:1)
[Warning][Deadcode] Function 'input_get_drvdata' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3376:1-3382:1)
[Warning][Deadcode] Function 'input_set_drvdata' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3383:1-3389:1)
[Warning][Deadcode] Function 'input_report_key' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3393:1-3400:1)
[Warning][Deadcode] Function 'input_sync' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3401:1-3407:1)
[Warning][Deadcode] Function '__kmalloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3444:1-3447:1)
[Warning][Deadcode] Function 'kmalloc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3449:1-3455:1)
[Warning][Deadcode] Function 'kzalloc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3457:1-3463:1)
[Warning][Deadcode] Function 'seek_rc_map' is uncalled: 16 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3475:1-3505:1)
[Warning][Deadcode] Function 'rc_map_get' is uncalled: 14 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3506:1-3532:1)
[Warning][Deadcode] Function 'ir_create_table' is uncalled: 20 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3560:1-3595:1)
[Warning][Deadcode] Function 'ir_free_table' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3596:1-3604:1)
[Warning][Deadcode] Function 'ir_resize_table' is uncalled: 52 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3605:1-3698:1)
[Warning][Deadcode] Function 'ir_update_mapping' is uncalled: 42 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3699:1-3777:1)
[Warning][Deadcode] Function 'ir_establish_scancode' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3778:1-3828:1)
[Warning][Deadcode] Function 'ir_setkeycode' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3829:1-3871:1)
[Warning][Deadcode] Function 'ir_setkeytable' is uncalled: 28 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3872:1-3926:1)
[Warning][Deadcode] Function 'ir_lookup_by_scancode' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3927:1-3954:1)
[Warning][Deadcode] Function 'ir_getkeycode' is uncalled: 28 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:3955:1-4009:1)
[Warning][Deadcode] Function 'rc_g_keycode_from_table' is uncalled: 20 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4010:1-4049:1)
[Warning][Deadcode] Function 'ir_do_keyup' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4050:1-4080:1)
[Warning][Deadcode] Function 'rc_keyup' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4081:1-4091:1)
[Warning][Deadcode] Function 'ir_timer_keyup' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4092:1-4107:1)
[Warning][Deadcode] Function 'rc_repeat' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4108:1-4128:1)
[Warning][Deadcode] Function 'ir_do_keydown' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4129:1-4166:1)
[Warning][Deadcode] Function 'rc_keydown' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4167:1-4188:1)
[Warning][Deadcode] Function 'rc_keydown_notimeout' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4189:1-4203:1)
[Warning][Deadcode] Function 'ir_open' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4204:1-4214:1)
[Warning][Deadcode] Function 'ir_close' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4215:1-4227:1)
[Warning][Deadcode] Function 'rc_allocate_device' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4586:1-4624:1)
[Warning][Deadcode] Function 'rc_free_device' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4625:1-4641:1)
[Warning][Deadcode] Function 'rc_register_device' is uncalled: 102 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4642:1-4824:1)
[Warning][Deadcode] Function 'rc_unregister_device' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4825:1-4859:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_1' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5052:1-5059:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5060:1-5067:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_3' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5068:1-5075:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_4' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5076:1-5087:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_5' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5088:1-5095:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_10' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5128:1-5135:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_11' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5136:1-5143:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_12' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5144:1-5151:1)
[Warning][Deadcode] Function 'INIT_LIST_HEAD' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5152:1-5159:1)
[Warning][Deadcode] Function 'get_current' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5162:1-5184:1)
[Warning][Deadcode] Function 'PTR_ERR' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5186:1-5191:1)
[Warning][Deadcode] Function 'IS_ERR' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5192:1-5198:1)
[Warning][Deadcode] Function 'spin_lock_irq' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5227:1-5233:1)
[Warning][Deadcode] Function 'spin_unlock_irq' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5234:1-5240:1)
[Warning][Deadcode] Function '__kfifo_uint_must_check_helper' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5250:1-5255:1)
[Warning][Deadcode] Function '__kfifo_int_must_check_helper' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5256:1-5261:1)
[Warning][Deadcode] Function 'init_ir_raw_event' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5269:1-5275:1)
[Warning][Deadcode] Function 'ir_raw_event_reset' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5281:1-5294:1)
[Warning][Deadcode] Function 'ir_raw_event_thread' is uncalled: 82 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5305:1-5451:1)
[Warning][Deadcode] Function 'ir_raw_event_store' is uncalled: 30 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5452:1-5511:1)
[Warning][Deadcode] Function 'ir_raw_event_store_edge' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5512:1-5556:1)
[Warning][Deadcode] Function 'ir_raw_event_store_with_filter' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5557:1-5586:1)
[Warning][Deadcode] Function 'ir_raw_event_set_idle' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5587:1-5630:1)
[Warning][Deadcode] Function 'ir_raw_event_handle' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5631:1-5645:1)
[Warning][Deadcode] Function 'ir_raw_event_register' is uncalled: 44 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5655:1-5736:1)
[Warning][Deadcode] Function 'ir_raw_event_unregister' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5737:1-5776:1)
[Warning][Deadcode] Function 'ir_raw_handler_register' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5777:1-5805:1)
[Warning][Deadcode] Function 'ir_raw_handler_unregister' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5806:1-5834:1)
[Warning][Deadcode] Function 'init_decoders' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5835:1-5848:1)
[Warning][Deadcode] Function 'ir_raw_init' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5849:1-5862:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_25' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5863:1-5870:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_26' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5871:1-5878:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_27' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5879:1-5886:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_28' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5887:1-5894:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_29' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5895:1-5902:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_30' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5903:1-5914:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_31' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5915:1-5922:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_32' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5923:1-5930:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_33' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5931:1-5938:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_36' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5955:1-5962:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_37' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5963:1-5970:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_38' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5971:1-5978:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_39' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5979:1-5986:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_40' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5987:1-5994:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_41' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5995:1-6002:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_42' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6003:1-6010:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_43' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6011:1-6018:1)
[Warning][Deadcode] Function 'ldv__builtin_expect' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6027:1-6032:1)
[Warning][Deadcode] Function 'ldv__builtin_trap' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6033:1-6039:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_interruptible_cred_guard_mutex_of_signal_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6041:1-6056:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_killable_cred_guard_mutex_of_signal_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6057:1-6072:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_cred_guard_mutex_of_signal_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6073:1-6083:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_cred_guard_mutex_of_signal_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6084:1-6099:1)
[Warning][Deadcode] Function 'ldv_atomic_dec_and_mutex_lock_cred_guard_mutex_of_signal_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6100:1-6116:1)
[Warning][Deadcode] Function 'ldv_mutex_is_locked_cred_guard_mutex_of_signal_struct' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6117:1-6131:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_cred_guard_mutex_of_signal_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6132:1-6142:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_interruptible_ir_raw_handler_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6144:1-6159:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_killable_ir_raw_handler_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6160:1-6175:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_ir_raw_handler_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6187:1-6202:1)
[Warning][Deadcode] Function 'ldv_atomic_dec_and_mutex_lock_ir_raw_handler_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6203:1-6218:1)
[Warning][Deadcode] Function 'ldv_mutex_is_locked_ir_raw_handler_lock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6219:1-6233:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_interruptible_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6246:1-6261:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_killable_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6262:1-6277:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_lock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6278:1-6288:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6289:1-6304:1)
[Warning][Deadcode] Function 'ldv_atomic_dec_and_mutex_lock_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6305:1-6320:1)
[Warning][Deadcode] Function 'ldv_mutex_is_locked_lock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6321:1-6335:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_lock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6336:1-6346:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_interruptible_lock_of_rc_dev' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6348:1-6363:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_killable_lock_of_rc_dev' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6364:1-6379:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_lock_of_rc_dev' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6391:1-6406:1)
[Warning][Deadcode] Function 'ldv_atomic_dec_and_mutex_lock_lock_of_rc_dev' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6407:1-6422:1)
[Warning][Deadcode] Function 'ldv_mutex_is_locked_lock_of_rc_dev' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6423:1-6437:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_interruptible_mutex_of_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6450:1-6465:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_killable_mutex_of_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6466:1-6481:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_mutex_of_device' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6482:1-6492:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_mutex_of_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6493:1-6508:1)
[Warning][Deadcode] Function 'ldv_atomic_dec_and_mutex_lock_mutex_of_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6509:1-6524:1)
[Warning][Deadcode] Function 'ldv_mutex_is_locked_mutex_of_device' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6525:1-6539:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_mutex_of_device' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6540:1-6550:1)
[Warning][Deadcode] Function '__dynamic_pr_debug' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6593:1-6595:1)
[Warning][Deadcode] Function '__init_work' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6596:1-6598:1)
[Warning][Deadcode] Function '__kfifo_alloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6600:1-6602:1)
[Warning][Deadcode] Function '__kfifo_free' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6603:1-6605:1)
[Warning][Deadcode] Function '__kfifo_in' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6607:1-6609:1)
[Warning][Deadcode] Function '__kfifo_in_r' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6611:1-6613:1)
[Warning][Deadcode] Function '__kfifo_out' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6615:1-6617:1)
[Warning][Deadcode] Function '__kfifo_out_r' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6619:1-6621:1)
[Warning][Deadcode] Function '__module_get' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6625:1-6627:1)
[Warning][Deadcode] Function '__mutex_init' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6628:1-6630:1)
[Warning][Deadcode] Function '__raw_spin_lock_init' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6631:1-6633:1)
[Warning][Deadcode] Function '__request_module' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6635:1-6637:1)
[Warning][Deadcode] Function '_raw_spin_lock_irq' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6641:1-6643:1)
[Warning][Deadcode] Function '_raw_spin_unlock_irq' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6651:1-6653:1)
[Warning][Deadcode] Function 'del_timer_sync' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6665:1-6667:1)
[Warning][Deadcode] Function 'dev_get_drvdata' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6668:1-6670:1)
[Warning][Deadcode] Function 'dev_set_drvdata' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6672:1-6674:1)
[Warning][Deadcode] Function 'dev_set_name' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6676:1-6678:1)
[Warning][Deadcode] Function 'device_add' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6680:1-6682:1)
[Warning][Deadcode] Function 'device_del' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6683:1-6685:1)
[Warning][Deadcode] Function 'device_initialize' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6686:1-6688:1)
[Warning][Deadcode] Function 'init_timer_key' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6689:1-6691:1)
[Warning][Deadcode] Function 'input_event' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6692:1-6694:1)
[Warning][Deadcode] Function 'input_free_device' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6695:1-6697:1)
[Warning][Deadcode] Function 'input_register_device' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6699:1-6701:1)
[Warning][Deadcode] Function 'input_scancode_to_scalar' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6703:1-6705:1)
[Warning][Deadcode] Function 'input_unregister_device' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6706:1-6708:1)
[Warning][Deadcode] Function 'kobject_get_path' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6712:1-6714:1)
[Warning][Deadcode] Function 'kthread_create_on_node' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6715:1-6717:1)
[Warning][Deadcode] Function 'kthread_should_stop' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6719:1-6721:1)
[Warning][Deadcode] Function 'kthread_stop' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6723:1-6725:1)
[Warning][Deadcode] Function 'ktime_get' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6726:1-6728:1)
[Warning][Deadcode] Function 'lockdep_init_map' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6736:1-6738:1)
[Warning][Deadcode] Function 'mod_timer' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6740:1-6742:1)
[Warning][Deadcode] Function 'module_put' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6743:1-6745:1)
[Warning][Deadcode] Function 'msecs_to_jiffies' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6747:1-6749:1)
[Warning][Deadcode] Function 'msleep' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6750:1-6752:1)
[Warning][Deadcode] Function 'mutex_trylock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6757:1-6759:1)
[Warning][Deadcode] Function 'put_device' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6767:1-6769:1)
[Warning][Deadcode] Function 'schedule' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6770:1-6772:1)
[Warning][Deadcode] Function 'schedule_work' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6774:1-6776:1)
[Warning][Deadcode] Function 'wake_up_process' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6785:1-6787:1)
[Warning][Deadcode] Function 'kfree' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6789:1-6791:1)
[Warning][Deadcode] Function 'ldv_check_final_state' has dead code:
  on line 6567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6567-6567)
  on line 6571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6571-6571)
  on line 6575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6575-6575)
  on line 6583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6583-6583)
[Warning][Deadcode] Function 'ldv_error' has dead code:
  on line 6025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6025-6025)
[Warning][Deadcode] Function 'ldv_mutex_lock_ir_raw_handler_lock' has dead code:
  on line 6181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6181-6181)
[Warning][Deadcode] Function 'ldv_mutex_unlock_ir_raw_handler_lock' has dead code:
  on line 6239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6239-6239)
[Warning][Deadcode] Function 'ldv_mutex_unlock_lock_of_rc_dev' has dead code:
  on line 6443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6443-6443)
[Warning][Deadcode] Function 'show_protocols' has dead code:
  on lines 4284..4292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4284-4292)
[Warning][Deadcode] Function 'store_protocols' has dead code:
  on lines 4374..4382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4374-4382)
  on lines 4429..4437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4429-4437)
  on lines 4466..4474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4466-4474)
  on lines 4488..4496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4488-4496)
  on lines 4517..4525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4517-4525)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 340
  dead: 1286 (1224 in uncalled functions)
  total lines: 1626
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_2 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5021:9-5021:34)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_2 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5029:9-5029:34)
[Warning][Deadcode][CWE-570] condition 'rc_core_debug > 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4428:9-4428:26)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:12:73-12:74)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_cred_guard_mutex_of_signal_struct == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6565:7-6565:55)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_ir_raw_handler_lock == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6569:7-6569:41)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_lock == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6573:7-6573:26)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_mutex_of_device == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6581:7-6581:37)
[Warning][Deadcode][CWE-570] condition 'rc_core_debug > 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4283:7-4283:24)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_0 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4962:7-4962:32)
[Warning][Deadcode][CWE-570] condition 'rc_core_debug > 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4465:9-4465:26)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_ir_raw_handler_lock == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6179:7-6179:41)
[Warning][Deadcode][CWE-570] condition 'rc_core_debug > 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4487:11-4487:28)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_lock_of_rc_dev == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6441:7-6441:36)
[Warning][Deadcode][CWE-570] condition 'rc_core_debug > 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4516:7-4516:24)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_ir_raw_handler_lock == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:6237:7-6237:41)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:5003:9-5003:34)
[Warning][Deadcode][CWE-570] condition 'rc_core_debug > 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--media--rc--rc-core.ko-main.cil.out.i:4373:9-4373:26)
[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
[Warning][Unsound][Call] No suitable function to call
[Error][Imprecise][Unsound] Function definition missing
