./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-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] Setting "ana.int.interval" to true
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain ONLY for:
[Info] writeb, printk, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp___0, tmp___1, exp, tmp___0, tmp, tmp___1, var_group1, var_group2, var_ni6527_interrupt_3_p0, var_ni6527_interrupt_3_p1, retval, tmp, dev, dev, tmp, bus, slot, mite, i, tmp, dev, ret, s, dev, tmp___0, err, tmp, cmd, dev, s, s, interval, dev, i, num_subdevices, dev, val, ret, size, tmp, n, size, tmp, size, s, flags, ret, tmp, tmp___0, tmp___1, size, flags, order, ret, size, tmp, size, res, tmp, tmp___0, tmp___1, tmp___2, cond, index, size, tmp, size, tmp, tmp___0, tmp___1, it_func_ptr, call_site, ptr, bytes_req, bytes_alloc, irq, handler, flags, name, dev, tmp, size, order
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2236:3-2236:51)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2236:3-2236:51)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2236:3-2236:51)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2242:3-2242:86)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2242:3-2242:86)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2242:3-2242:86)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2310:3-2310:73)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1921:3-1921:28)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1922:3-1922:105)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1922:3-1922:105)
[Info][Unsound] ASM statement ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1735:3-1735:97)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1932:3-1932:97)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1932:3-1932:97)
[Info][Unsound] ASM statement ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1742:3-1742:98)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1933:3-1933:30)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1934:4-1934:47)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1935:3-1935:23)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2305:3-2305:28)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2145:8-2145:289)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2145:8-2145:289)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2145:8-2145:289)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2146:5-2146:99)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2146:5-2146:99)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2149:7-2149:21)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2150:5-2150:36)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2150:5-2150:36)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2153:7-2153:176)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2153:7-2153:176)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2154:5-2154:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2154:5-2154:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2301:3-2301:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2075:3-2075:46)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2076:3-2076:31)
[Error][Imprecise][Unsound] Function definition missing for kmem_cache_alloc_notrace (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1697:7-1697:47)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1785:3-1785:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1786:7-1786:66)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2081:3-2081:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2081:3-2081:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2174:9-2174:114)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2174:9-2174:114)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2174:9-2174:114)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2174:9-2174:114)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2183:3-2183:29)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1808:11-1808:49)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2185:5-2185:73)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2186:6-2186:57)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2086:3-2086:66)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2086:3-2086:66)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2092:3-2092:72)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2093:3-2093:104)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2093:3-2093:104)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2094:3-2094:73)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2094:3-2094:73)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2095:3-2095:34)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1757:3-1757:43)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1759:3-1759:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1760:7-1760:88)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1767:4-1767:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1768:4-1768:59)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1769:3-1769:69)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1769:3-1769:69)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1770:3-1771:75)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1770:3-1771:75)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1772:4-1772:52)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2100:3-2100:22)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2101:3-2101:14)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2102:3-2102:26)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2103:3-2103:17)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2104:3-2104:37)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2105:3-2105:18)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2106:3-2106:43)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2107:3-2107:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2108:3-2108:28)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2115:3-2115:28)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2116:3-2116:23)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2127:3-2127:97)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2127:3-2127:97)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2128:3-2128:97)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2128:3-2128:97)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2129:3-2129:97)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2129:3-2129:97)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2130:3-2130:97)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2130:3-2130:97)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2131:3-2131:97)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2131:3-2131:97)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2132:3-2132:68)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2132:3-2132:68)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1802:12-1802:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2133:3-2133:79)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1453:3-1453:64)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2137:5-2137:71)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2137:5-2137:71)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2250:3-2250:44)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2250:3-2250:44)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2250:3-2250:44)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:12:1-12:214)
[Warning][Deadcode] Function 'get_order' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1407:1-1422:1)
[Warning][Deadcode] Function 'rcu_read_lock_sched_held' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1433:1-1438:1)
[Warning][Deadcode] Function 'rcu_read_lock_sched_notrace' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1439:1-1444:1)
[Warning][Deadcode] Function 'kmemleak_alloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1459:1-1465:1)
[Warning][Deadcode] Function 'trace_kmalloc' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1467:1-1519:1)
[Warning][Deadcode] Function 'kmalloc_index' is uncalled: 47 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1521:1-1618:1)
[Warning][Deadcode] Function 'kmalloc_slab' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1619:1-1632:1)
[Warning][Deadcode] Function 'kmalloc_large' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1658:1-1674:1)
[Warning][Deadcode] Function 'ni6527_di_insn_config' is uncalled: 20 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1825:1-1863:1)
[Warning][Deadcode] Function 'ni6527_di_insn_bits' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1864:1-1883:1)
[Warning][Deadcode] Function 'ni6527_do_insn_bits' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1884:1-1912:1)
[Warning][Deadcode] Function 'ni6527_intr_cmdtest' is uncalled: 45 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1939:1-2019:1)
[Warning][Deadcode] Function 'ni6527_intr_cmd' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2020:1-2027:1)
[Warning][Deadcode] Function 'ni6527_intr_cancel' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2028:1-2034:1)
[Warning][Deadcode] Function 'ni6527_intr_insn_bits' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2035:1-2046:1)
[Warning][Deadcode] Function 'ni6527_intr_insn_config' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2047:1-2067:1)
[Warning][Deadcode] Function 'driver_ni6527_pci_probe' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2208:1-2215:1)
[Warning][Deadcode] Function 'driver_ni6527_pci_remove' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2216:1-2222:1)
[Warning][Deadcode] Function 'ldv_error' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2330:1-2335:1)
[Warning][Deadcode] Function 'ldv__builtin_expect' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2336:1-2341:1)
[Warning][Deadcode] Function '__get_free_pages' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2367:1-2369:1)
[Warning][Deadcode] Function 'comedi_pci_auto_config' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2393:1-2395:1)
[Warning][Deadcode] Function 'comedi_pci_auto_unconfig' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2396:1-2398:1)
[Warning][Deadcode] Function 'debug_lockdep_rcu_enabled' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2400:1-2402:1)
[Warning][Deadcode] Function 'lockdep_rcu_dereference' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2412:1-2414:1)
[Warning][Deadcode] Function 'kfree' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2437:1-2439:1)
[Warning][Deadcode] Function 'kcalloc' has dead code:
  on line 1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1715-1715)
[Warning][Deadcode] Function 'kmalloc' has dead code:
  on lines 1685..1687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1685-1687)
  on lines 1690..1694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1690-1694)
  on lines 1697..1698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1697-1698)
  on line 1700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1700-1700)
[Warning][Deadcode] Function 'ldv_check_final_state' has dead code:
  on line 2351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2351-2351)
  on line 2356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2356-2356)
  on line 2361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2361-2361)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 235
  dead: 228 (213 in uncalled functions)
  total lines: 463
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1684:7-1684:8)
[Warning][Deadcode][CWE-571] condition 'size != 0UL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1714:7-1714:53)
[Warning][Deadcode][CWE-570] condition '0xffffffffffffffffUL / size < n' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:1714:7-1714:53)
[Warning][Deadcode][CWE-571] condition 'tmp == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2349:7-2349:15)
[Warning][Deadcode][CWE-571] condition 'tmp___0 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2354:7-2354:19)
[Warning][Deadcode][CWE-571] condition 'tmp___1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36.i:2359:7-2359:19)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
[Info][Unsound] ASM ignored
[Error][Imprecise][Unsound] Function definition missing
