./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_670x-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] printk, writel, 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___0, tmp___1, exp, tmp___0, tmp, tmp___1, var_group1, var_group2, bus, slot, mite, i, tmp, dev, s, s, i, i, chan, ret, s, i, tmp, dev, range_table_list, retval, tmp, dev, dev, tmp, 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, 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_670x-ko--107_1a--adbbc36.i:1840:3-1840:52)
[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_670x-ko--107_1a--adbbc36.i:1840:3-1840:52)
[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_670x-ko--107_1a--adbbc36.i:1840:3-1840:52)
[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_670x-ko--107_1a--adbbc36.i:1846:3-1846:87)
[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_670x-ko--107_1a--adbbc36.i:1846:3-1846:87)
[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_670x-ko--107_1a--adbbc36.i:1846:3-1846:87)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:2142:3-2142: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_670x-ko--107_1a--adbbc36.i:1948:3-1948:55)
[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_670x-ko--107_1a--adbbc36.i:1949:3-1949:59)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1949:3-1949:59)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)p in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:2258:3-2258: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_670x-ko--107_1a--adbbc36.i:1950:7-1950:177)
[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_670x-ko--107_1a--adbbc36.i:1950:7-1950:177)
[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_670x-ko--107_1a--adbbc36.i:1951:5-1951:65)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1951:5-1951:65)
[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_670x-ko--107_1a--adbbc36.i:1954:7-1954: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_670x-ko--107_1a--adbbc36.i:1955:5-1955: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_670x-ko--107_1a--adbbc36.i:1955:5-1955: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_670x-ko--107_1a--adbbc36.i:2138:3-2138:41)
[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_670x-ko--107_1a--adbbc36.i:1877:3-1877: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_670x-ko--107_1a--adbbc36.i:1878:3-1878:32)
[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_670x-ko--107_1a--adbbc36.i:1682:7-1682: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_670x-ko--107_1a--adbbc36.i:1770:3-1770: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_670x-ko--107_1a--adbbc36.i:1771:7-1771: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_670x-ko--107_1a--adbbc36.i:1883:3-1883:65)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1883:3-1883:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:2059:9-2059: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_670x-ko--107_1a--adbbc36.i:2059:9-2059: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_670x-ko--107_1a--adbbc36.i:2059:9-2059: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_670x-ko--107_1a--adbbc36.i:2059:9-2059: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_670x-ko--107_1a--adbbc36.i:2068:3-2068: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_670x-ko--107_1a--adbbc36.i:1792:11-1792: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_670x-ko--107_1a--adbbc36.i:2070:5-2070:74)
[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_670x-ko--107_1a--adbbc36.i:2071:6-2071:58)
[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_670x-ko--107_1a--adbbc36.i:1888:3-1888:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1888:3-1888:67)
[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_670x-ko--107_1a--adbbc36.i:1894:3-1894:67)
[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_670x-ko--107_1a--adbbc36.i:1895:3-1895:70)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1895:3-1895:70)
[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_670x-ko--107_1a--adbbc36.i:1786:12-1786:31)
[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_670x-ko--107_1a--adbbc36.i:1896:3-1896: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_670x-ko--107_1a--adbbc36.i:1896:3-1896: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_670x-ko--107_1a--adbbc36.i:1897:3-1897: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_670x-ko--107_1a--adbbc36.i:1742:3-1742: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_670x-ko--107_1a--adbbc36.i:1744:3-1744: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_670x-ko--107_1a--adbbc36.i:1745:7-1745: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_670x-ko--107_1a--adbbc36.i:1752:4-1752: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_670x-ko--107_1a--adbbc36.i:1753:4-1753: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_670x-ko--107_1a--adbbc36.i:1754:3-1754: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_670x-ko--107_1a--adbbc36.i:1754:3-1754: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_670x-ko--107_1a--adbbc36.i:1755:3-1756: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_670x-ko--107_1a--adbbc36.i:1755:3-1756: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_670x-ko--107_1a--adbbc36.i:1757:4-1757: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_670x-ko--107_1a--adbbc36.i:1902:3-1902: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_670x-ko--107_1a--adbbc36.i:1903:3-1903: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_670x-ko--107_1a--adbbc36.i:1904:3-1904:27)
[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_670x-ko--107_1a--adbbc36.i:1905:3-1905:71)
[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_670x-ko--107_1a--adbbc36.i:1906:3-1906: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_670x-ko--107_1a--adbbc36.i:1907:7-1907: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_670x-ko--107_1a--adbbc36.i:1914:5-1914:81)
[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_670x-ko--107_1a--adbbc36.i:1927:5-1927: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_670x-ko--107_1a--adbbc36.i:1929:3-1929: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_670x-ko--107_1a--adbbc36.i:1930:3-1930: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_670x-ko--107_1a--adbbc36.i:1931:3-1931: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_670x-ko--107_1a--adbbc36.i:1939:3-1939:100)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1939:3-1939:100)
[Info][Unsound] ASM statement ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1728:3-1728: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_670x-ko--107_1a--adbbc36.i:1940:3-1940: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_670x-ko--107_1a--adbbc36.i:1940:3-1940:99)
[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_670x-ko--107_1a--adbbc36.i:1854:3-1854:45)
[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_670x-ko--107_1a--adbbc36.i:1854:3-1854:45)
[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_670x-ko--107_1a--adbbc36.i:1854:3-1854:45)
[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_670x-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_670x-ko--107_1a--adbbc36.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_670x-ko--107_1a--adbbc36.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_670x-ko--107_1a--adbbc36.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_670x-ko--107_1a--adbbc36.i:1444:1-1450: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_670x-ko--107_1a--adbbc36.i:1452:1-1504: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_670x-ko--107_1a--adbbc36.i:1506:1-1603: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_670x-ko--107_1a--adbbc36.i:1604:1-1617: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_670x-ko--107_1a--adbbc36.i:1643:1-1659:1)
[Warning][Deadcode] Function 'readl' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1717:1-1724:1)
[Warning][Deadcode] Function 'driver_ni_670x_pci_probe' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1809:1-1816:1)
[Warning][Deadcode] Function 'driver_ni_670x_pci_remove' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1817:1-1823:1)
[Warning][Deadcode] Function 'ni_670x_ao_winsn' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1961:1-1982:1)
[Warning][Deadcode] Function 'ni_670x_ao_rinsn' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1983:1-2002:1)
[Warning][Deadcode] Function 'ni_670x_dio_insn_bits' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:2003:1-2020:1)
[Warning][Deadcode] Function 'ni_670x_dio_insn_config' is uncalled: 14 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:2021:1-2044: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_670x-ko--107_1a--adbbc36.i:2161:1-2166: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_670x-ko--107_1a--adbbc36.i:2167:1-2172: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_670x-ko--107_1a--adbbc36.i:2198:1-2200: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_670x-ko--107_1a--adbbc36.i:2217:1-2219: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_670x-ko--107_1a--adbbc36.i:2220:1-2222: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_670x-ko--107_1a--adbbc36.i:2224:1-2226: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_670x-ko--107_1a--adbbc36.i:2236:1-2238:1)
[Warning][Deadcode] Function 'kcalloc' has dead code:
  on line 1700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1700-1700)
[Warning][Deadcode] Function 'kmalloc' has dead code:
  on lines 1670..1672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1670-1672)
  on lines 1675..1679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1675-1679)
  on lines 1682..1683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1682-1683)
  on line 1685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:1685-1685)
[Warning][Deadcode] Function 'ldv_check_final_state' has dead code:
  on line 2182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:2182-2182)
  on line 2187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:2187-2187)
  on line 2192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36.i:2192-2192)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 200
  dead: 161 (146 in uncalled functions)
  total lines: 361
[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_670x-ko--107_1a--adbbc36.i:1669:7-1669: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_670x-ko--107_1a--adbbc36.i:1699:7-1699: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_670x-ko--107_1a--adbbc36.i:1699:7-1699: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_670x-ko--107_1a--adbbc36.i:2180:7-2180: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_670x-ko--107_1a--adbbc36.i:2185:7-2185: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_670x-ko--107_1a--adbbc36.i:2190:7-2190:19)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
[Info][Unsound] ASM ignored
[Error][Imprecise][Unsound] Function definition missing
