./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-1.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, 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-1.i:2233:3-2233: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-1.i:2233:3-2233: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-1.i:2233:3-2233: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-1.i:2239:3-2239: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-1.i:2239:3-2239: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-1.i:2239:3-2239: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-1.i:2289:3-2289: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-1.i:1918:3-1918: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-1.i:1919:3-1919: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-1.i:1919:3-1919: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-1.i:1732:3-1732: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-1.i:1929:3-1929: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-1.i:1929:3-1929: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-1.i:1739:3-1739: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-1.i:1930:3-1930: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-1.i:1931:4-1931: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-1.i:1932:3-1932: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-1.i:2284:3-2284: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-1.i:2142:8-2142: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-1.i:2142:8-2142: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-1.i:2142:8-2142: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-1.i:2143:5-2143: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-1.i:2143:5-2143: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-1.i:2146:7-2146: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-1.i:2147:5-2147: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-1.i:2147:5-2147: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-1.i:2150:7-2150: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-1.i:2150:7-2150: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-1.i:2151:5-2151: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-1.i:2151:5-2151: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-1.i:2280:3-2280: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-1.i:2072:3-2072: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-1.i:2073:3-2073: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-1.i:1694:7-1694: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-1.i:1782:3-1782: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-1.i:1783:7-1783: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-1.i:2078:3-2078: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-1.i:2078:3-2078: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-1.i:2171:9-2171: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-1.i:2171:9-2171: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-1.i:2171:9-2171: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-1.i:2171:9-2171: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-1.i:2180:3-2180: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-1.i:1805:11-1805: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-1.i:2182:5-2182: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-1.i:2183:6-2183: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-1.i:2083:3-2083: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-1.i:2083:3-2083: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-1.i:2089:3-2089: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-1.i:2090:3-2090: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-1.i:2090:3-2090: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-1.i:2091:3-2091: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-1.i:2091:3-2091: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-1.i:2092:3-2092: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-1.i:1754:3-1754: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-1.i:1756:3-1756: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-1.i:1757:7-1757: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-1.i:1764:4-1764: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-1.i:1765:4-1765: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-1.i:1766:3-1766: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-1.i:1766:3-1766: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-1.i:1767:3-1768: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-1.i:1767:3-1768: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-1.i:1769:4-1769: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-1.i:2097:3-2097: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-1.i:2098:3-2098: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-1.i:2099:3-2099: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-1.i:2100:3-2100: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-1.i:2101:3-2101: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-1.i:2102:3-2102: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-1.i:2103:3-2103: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-1.i:2104:3-2104: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-1.i:2105:3-2105: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-1.i:2112:3-2112: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-1.i:2113:3-2113: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-1.i:2124:3-2124: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-1.i:2124:3-2124: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-1.i:2125:3-2125: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-1.i:2125:3-2125: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-1.i:2126:3-2126: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-1.i:2126:3-2126: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-1.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-1.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-1.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-1.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-1.i:2129:3-2129: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-1.i:2129:3-2129: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-1.i:1799:12-1799: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-1.i:2130:3-2130: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-1.i:1450:3-1450: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-1.i:2134:5-2134: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-1.i:2134:5-2134: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-1.i:2247:3-2247: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-1.i:2247:3-2247: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-1.i:2247:3-2247:44)
[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-1.i:1404:1-1419: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-1.i:1430:1-1435: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-1.i:1436:1-1441: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-1.i:1456:1-1462: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-1.i:1464:1-1516: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-1.i:1518:1-1615: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-1.i:1616:1-1629: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-1.i:1655:1-1671: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-1.i:1822:1-1860: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-1.i:1861:1-1880: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-1.i:1881:1-1909: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-1.i:1936:1-2016: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-1.i:2017:1-2024: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-1.i:2025:1-2031: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-1.i:2032:1-2043: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-1.i:2044:1-2064: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-1.i:2205:1-2212: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-1.i:2213:1-2219: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-1.i:2315:1-2320: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-1.i:2349:1-2351: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-1.i:2375:1-2377: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-1.i:2378:1-2380: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-1.i:2382:1-2384: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-1.i:2406:1-2408: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-1.i:2431:1-2433:1)
[Warning][Deadcode] Function 'kcalloc' has dead code:
  on line 1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36-1.i:1712-1712)
[Warning][Deadcode] Function 'kmalloc' has dead code:
  on lines 1682..1684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36-1.i:1682-1684)
  on lines 1687..1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36-1.i:1687-1691)
  on lines 1694..1695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36-1.i:1694-1695)
  on line 1697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36-1.i:1697-1697)
[Warning][Deadcode] Function 'ldv_error' has dead code:
  on line 2314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36-1.i:2314-2314)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 241
  dead: 223 (210 in uncalled functions)
  total lines: 464
[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-1.i:12:73-12:74)
[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-1.i:1681:7-1681: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-1.i:1711:7-1711: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-1.i:1711:7-1711:53)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
[Info][Unsound] ASM ignored
[Error][Imprecise][Unsound] Function definition missing
