./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] Setting "ana.int.interval" to true
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain ONLY for:
[Info] ldv_state_variable_1, ldv_state_variable_2, i, count, tmp, key, a, count, i, j, i___0, j___0, k, size, r, top, expression, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tty, tty, arg, ldv_func_arg1, ldv_func_arg2, ldv_func_arg3, ldv_func_res, tmp, ldv_func_arg1, ldv_func_arg2, ldv_func_arg4, tmp, tmp___4, tmp___6, tmp___3, tmp___5, ldvarg0, ldvarg2, tmp___1, ldvarg4, retval, retval, nintf, ifnum, tmp___0, tmp___1, data, serial, tmp, driver, tmp, tmp, tmp___0, epd, tmp___1, tmp, tmp___0, epd, tmp___1, exp, tmp, tmp, p, tmp___0, size, tmp, p, tmp___0, size, tmp, cond, size, tmp, size, s, flags, ret, tmp, tmp___0, tmp___1, size, flags, order, ret, size, tmp, index, size, tmp, size, tmp, tmp___0, tmp___1, it_func_ptr, call_site, ptr, bytes_req, bytes_alloc, size, order
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )

[Info] runtime: 00:00:10.343
[Info] vars: 13519, evals: 17538

[Info] |called|=22

Memory statistics: total=16647.40MB, max=268.97MB, minor=16642.38MB, major=444.15MB, promoted=439.14MB
    minor collections=7944  major collections=17 compactions=0

[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5221:7-5221:56)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5211:7-5211:66)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5197:7-5197:45)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5199:7-5199:28)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5203:7-5203:45)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5205:7-5205:28)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5186:7-5186:94)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5189:9-5189:30)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4844:3-4844:43)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4844:3-4844:43)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4844:3-4844:43)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4483:3-4483:71)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4483:3-4483:71)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4483:3-4483:71)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5274:3-5274:73)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5274:3-5274:73)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5274:3-5274:73)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4899:3-4899:48)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4851:5-4851:38)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4851:5-4851:38)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4851:5-4851:38)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4886:3-4886:45)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4888:3-4888:49)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4890:3-4890:54)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5121:7-5121:54)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5129:7-5129:54)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5089:7-5089:48)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5094:7-5094:48)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5099:7-5099:48)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5104:7-5104:48)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5109:7-5109:48)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5114:7-5114:48)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5067:7-5067:43)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5072:7-5072:43)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5077:7-5077:43)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5082:7-5082:43)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5059:7-5059:40)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5061:7-5061:28)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5027:7-5027:43)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5032:7-5032:43)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5037:7-5037:43)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5042:7-5042:43)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5047:7-5047:43)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5052:7-5052:43)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5009:7-5009:69)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5017:7-5017:69)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4991:7-4991:64)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4999:7-4999:64)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4979:7-4979:38)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4984:7-4984:38)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4969:7-4969:55)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4958:7-4958:85)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4710:3-4710:45)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4717:3-4717:58)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4723:3-4723:38)
[Error][Imprecise][Unsound] Function definition missing for kmem_cache_alloc_notrace (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4298:7-4298:47)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4730:3-4730:24)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4730:3-4730:24)
[Warning][Unknown] lval (& data)->susp_lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4055:11-4055:34)
[Warning][Unknown] lval (& data)->susp_lock.ldv_5784.rlock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5342:3-5342:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4739:3-4739:38)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4739:3-4739:38)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4742:8-4742:48)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4743:5-4743:49)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4745:8-4745:47)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4749:7-4749:52)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4750:5-4750:106)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4750:5-4750:106)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4440:3-4440:36)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4431:12-4431:46)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4442:5-4442:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4419:11-4419:59)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4419:11-4419:59)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4752:7-4752:115)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4752:7-4752:115)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4460:3-4460:36)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4462:5-4462:40)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4425:11-4425:60)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4758:14-4758:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4762:9-4762:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4762:9-4762:64)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4764:11-4765:26)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4764:11-4765:26)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4798:5-4798:60)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4798:5-4798:60)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4800:7-4801:22)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4800:7-4801:22)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4824:3-4825:23)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4824:3-4825:23)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4785:5-4785:60)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4785:5-4785:60)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4787:7-4788:22)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4787:7-4788:22)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4813:5-4813:60)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4813:5-4813:60)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4815:7-4816:22)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4815:7-4816:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4961:9-4961:30)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4944:7-4945:30)
[Info][Unsound] Unknown value in {&(alloc@sid:161)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4950:7-4951:30)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4862:3-4862:36)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4862:3-4862:36)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4862:3-4862:36)
[Warning][Deadcode] Function 'get_order' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4034:1-4049:1)
[Warning][Deadcode] Function 'rcu_read_lock_sched_held' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4060:1-4065:1)
[Warning][Deadcode] Function 'rcu_read_lock_sched_notrace' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4066:1-4071:1)
[Warning][Deadcode] Function 'kmemleak_alloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4079:1-4085:1)
[Warning][Deadcode] Function 'trace_kmalloc' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4087:1-4139:1)
[Warning][Deadcode] Function 'kmalloc_index' is uncalled: 47 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4141:1-4238:1)
[Warning][Deadcode] Function 'kmalloc_slab' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4239:1-4252:1)
[Warning][Deadcode] Function 'kmalloc_large' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4259:1-4275:1)
[Warning][Deadcode] Function 'ldv_undef_int' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4361:1-4368:1)
[Warning][Deadcode] Function 'ldv_undef_ulong' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4369:1-4376:1)
[Warning][Deadcode] Function 'ldv__builtin_expect' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4391:1-4396:1)
[Warning][Deadcode] Function 'ldv__builtin_trap' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4397:1-4403:1)
[Warning][Deadcode] Function 'ldv_tty_insert_flip_string_fixed_flag_4' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5257:1-5267:1)
[Warning][Deadcode] Function 'ldv_handler_precall' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5309:1-5319:1)
[Warning][Deadcode] Function 'ldv_got_tty' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5320:1-5326:1)
[Warning][Deadcode] Function 'ldv_check_tty' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5327:1-5336:1)
[Warning][Deadcode] Function '__get_free_pages' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5338:1-5340:1)
[Warning][Deadcode] Function 'debug_lockdep_rcu_enabled' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5345:1-5347:1)
[Warning][Deadcode] Function 'lockdep_rcu_dereference' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5359:1-5361:1)
[Warning][Deadcode] Function 'printk' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5363:1-5365:1)
[Warning][Deadcode] Function 'tty_insert_flip_string_fixed_flag' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5367:1-5369:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'kmalloc' has dead code:
  on lines 4286..4288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4286-4288)
  on lines 4291..4295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4291-4295)
  on lines 4298..4299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4298-4299)
  on line 4301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4301-4301)
[Warning][Deadcode] Function 'ldv_error' has dead code:
  on line 4383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4383-4383)
[Warning][Deadcode] Function 'main' has dead code:
  on line 5254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5254-5254)
[Warning][Deadcode] Function 'qcprobe' has dead code:
  on line 4713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4713-4713)
  on line 4719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4719-4719)
  on line 4725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4725-4725)
  on line 4755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4755-4755)
  on line 4782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4782-4782)
  on line 4795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4795-4795)
  on line 4810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4810-4810)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 400
  dead: 135 (115 in uncalled functions)
  total lines: 535
[Warning][Deadcode][CWE-570] condition 'debug != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4712:7-4712:17)
[Warning][Deadcode][CWE-570] condition 'debug != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4718:7-4718:17)
[Warning][Deadcode][CWE-570] condition 'debug != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4724:7-4724:17)
[Warning][Deadcode][CWE-571] condition 'usb_counter == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5196:9-5196:54)
[Warning][Deadcode][CWE-571] condition 'usb_counter == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5202:9-5202:54)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4285:7-4285:8)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:12:73-12:74)
[Warning][Deadcode][CWE-570] condition 'debug != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4754:13-4754:23)
[Warning][Deadcode][CWE-570] condition '! cond' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4325:6-4325:11)
[Warning][Deadcode][CWE-570] condition 'debug != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4781:9-4781:19)
[Warning][Deadcode][CWE-570] condition 'debug != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4794:9-4794:19)
[Warning][Deadcode][CWE-570] condition 'debug != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:4809:9-4809:19)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_0 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5145:7-5145:32)
[Warning][Deadcode][CWE-571] condition 'ldv_retval_5 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.i:5164:11-5164:28)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
[Error][Imprecise][Unsound] Function definition missing
