./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-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 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:34-996:2465 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2467-996:6154 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:9-996:6167 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:989:5-997:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:34-999:2454 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2456-999:3239 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:9-999:3252 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:642-1001:705 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:853-1001:942 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:944-1001:1304 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:13-1001:1351 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:998:5-1006:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1007:5-1009:5 with factor 2
[Info] Setting "ana.int.interval" to true
[Info] malloc wrapper: alt_malloc
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5013-996:5091)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5013-996:5091)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5106-996:5146)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5152-996:5216)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5222-996:5258)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5264-996:5350)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5354-996:5379)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5499-996:5537)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5541-996:5570)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5541-996:5570)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5541-996:5570)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5541-996:5570)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5541-996:5570)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5541-996:5570)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4882-996:4942)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]),[0,2147483647],not {} ([-31,31]))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1663-996:1702)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1663-996:1702)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]),[0,2147483647],not {} ([-31,31]))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1712-996:1751)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1712-996:1751)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]),[0,2147483647],not {} ([-31,31]))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1761-996:1799)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1761-996:1799)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1809-996:1828)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1837-996:1851)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1853-996:1871)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1903-996:1921)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1923-996:1937)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1939-996:1962)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1964-996:1982)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1984-996:2002)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2004-996:2032)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2034-996:2048)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2050-996:2068)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2070-996:2098)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2100-996:2118)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2120-996:2134)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2136-996:2160)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2162-996:2180)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2182-996:2200)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2202-996:2229)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2231-996:2245)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2247-996:2265)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2267-996:2294)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2296-996:2314)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2316-996:2330)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2332-996:2356)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2358-996:2376)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2378-996:2396)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2398-996:2426)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3357-996:3388)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3357-996:3388)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3357-996:3388)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3357-996:3388)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3357-996:3388)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3357-996:3388)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3427-996:3514)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3427-996:3514)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3427-996:3514)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3517-996:3552)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3517-996:3552)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3517-996:3552)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3517-996:3552)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3517-996:3552)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3517-996:3552)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3517-996:3552)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3555-996:3591)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3555-996:3591)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3555-996:3591)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3555-996:3591)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3555-996:3591)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3555-996:3591)
[Warning][Unknown] lval (& user)->id points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:951:5-951:48)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:951:5-951:48)
[Warning][Unknown] lval (& user)->id points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:951:5-951:48)
[Warning][Unknown] lval (& user)->id points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:953:9-953:55)
[Warning][Unknown] lval (& user)->id points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:941:1-941:1)
[Warning][Unknown] lval (& user)->id points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:955:12-955:22)
[Warning][Unknown] lval (& user)->id points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:955:12-955:22)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2676-996:2741)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2676-996:2741)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2676-996:2741)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2676-996:2741)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2676-996:2741)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2676-996:2741)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2785-996:2832)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2785-996:2832)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2785-996:2832)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2785-996:2832)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2785-996:2832)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2785-996:2832)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:974:5-974:22)
[Warning][Unknown] lval (& user)->id points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:976:1-976:1)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2835-996:2870)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2835-996:2870)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2835-996:2870)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2835-996:2870)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2835-996:2870)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2835-996:2870)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3007-996:3096)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3007-996:3096)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3007-996:3096)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3007-996:3096)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3007-996:3096)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3007-996:3096)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3238-996:3308)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3238-996:3308)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3238-996:3308)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3238-996:3308)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3238-996:3308)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3238-996:3308)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:975:5-975:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3632-996:3659)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3666-996:3729)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3764-996:3812)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3814-996:3831)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3834-996:3875)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3834-996:3875)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3834-996:3875)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3834-996:3875)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3834-996:3875)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3834-996:3875)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3955-996:3997)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4041-996:4130)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4041-996:4130)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4268-996:4386)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4431-996:4529)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4431-996:4529)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4431-996:4529)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4431-996:4529)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4431-996:4529)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4431-996:4529)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4431-996:4529)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4533-996:4756)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4533-996:4756)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4533-996:4756)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4533-996:4756)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5598-996:5703)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5598-996:5703)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5598-996:5703)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5598-996:5703)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5598-996:5703)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5598-996:5703)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5598-996:5703)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5707-996:5744)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5748-996:5786)
[Info][Unsound] Unknown address in {&(alloc@sid:8273)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5790-996:5835)
[Info][Unsound] Unknown address in {&(alloc@sid:45).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5790-996:5835)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5790-996:5835)
[Info][Unsound] Unknown address in {&(alloc@sid:45)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5790-996:5835)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:45).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:45).hh}
                                                       key -> {&(alloc@sid:45).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:45)}
                                                       prev -> {?, NULL, &(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]}
                                                       tbl -> {&(alloc@sid:8203)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5790-996:5835)
[Info][Unsound] Unknown value in {&(alloc@sid:45).hh[def_exc:Unknown int([-31,31]); intervals:[-2147483647,2147483647]; enums:not {} ([-31,31])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5790-996:5835)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5839-996:6002)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5839-996:6002)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:3072-999:3162)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:3072-999:3162)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]),[0,9],not {} ([-31,31]))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1652-999:1691)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1652-999:1691)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]),[0,9],not {} ([-31,31]))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1701-999:1740)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1701-999:1740)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]),[0,9],not {} ([-31,31]))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1750-999:1788)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1750-999:1788)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1798-999:1817)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1826-999:1840)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1842-999:1860)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1892-999:1910)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1912-999:1926)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1928-999:1951)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1953-999:1971)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1973-999:1991)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1993-999:2021)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2023-999:2037)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2039-999:2057)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2059-999:2087)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2089-999:2107)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2109-999:2123)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2125-999:2149)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2151-999:2169)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2171-999:2189)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2191-999:2218)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2220-999:2234)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2236-999:2254)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2256-999:2283)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2285-999:2303)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2305-999:2319)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2321-999:2345)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2347-999:2365)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2367-999:2385)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2387-999:2415)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2518-999:2581)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2518-999:2581)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2623-999:2681)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2691-999:2809)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2691-999:2809)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2966-999:3011)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:968:5-968:23)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:969:12-969:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:348-1001:383)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:348-1001:383)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:388-1001:487)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:388-1001:487)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:531-1001:631)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:531-1001:631)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:749-1001:849)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:749-1001:849)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:858-1001:929)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:858-1001:929)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:858-1001:929)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:964-1001:1012)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:964-1001:1012)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:1014-1001:1031)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:1149-1001:1202)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:1236-1001:1289)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:1307-1001:1334)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:1307-1001:1334)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:1307-1001:1334)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:148-1001:243)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:148-1001:243)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:148-1001:243)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:148-1001:243)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:959:12-959:61)
[Warning][Unknown] lval (& tmp)->hh points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:959:12-959:61)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer ptr in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:963:5-963:14)
[Warning][Unknown] lval (& tmp)->hh points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:964:1-964:1)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:245-1001:292)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:245-1001:292)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:245-1001:292)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Pointer ptr in function free doesn't evaluate to a valid address. Invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:963:5-963:14)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1002:13-1002:27)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer p in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:983:5-983:12)
[Warning][Unknown] lval (& tmp)->hh points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:984:1-984:1)
[Warning][Unknown] lval (& tmp)->hh points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:941:1-941:1)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:282:1-286:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:287:1-291:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:292:1-296:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:297:1-301:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:302:1-306:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:992-992)
[Warning][Deadcode] Function 'reach_error' has dead code:
  on line 936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:936-936)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 49
  dead: 7 (5 in uncalled functions)
  total lines: 56
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 10U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1363-999:1370)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 9U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1417-999:1423)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 8U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1469-999:1475)
[Warning][Deadcode][CWE-570] condition '_hj_k >= 12U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:234-996:246)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:940-1001:942)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 7U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1518-999:1524)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 6U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1567-999:1573)
[Warning][Deadcode][CWE-570] condition '! _he_new_buckets' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:4392-996:4408)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 5U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1615-999:1621)
[Warning][Deadcode][CWE-571] condition '_hj_k___0 == 4U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1644-999:1650)
[Warning][Deadcode][CWE-570] condition '_hj_k >= 12U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:234-996:246)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2426-999:2428)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2439-999:2441)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2452-999:2454)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 >= 12U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:223-999:235)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:1302-1001:1304)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:5102-996:5104)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2437-996:2439)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2450-996:2452)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2592-999:2594)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2463-996:2465)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2601-999:2608)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:6165-996:6167)
[Warning][Deadcode][CWE-570] condition '_hj_k == 11U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1319-996:1326)
[Warning][Deadcode][CWE-570] condition '_hj_k == 10U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1374-996:1381)
[Warning][Deadcode][CWE-570] condition '_hj_k == 9U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1428-996:1434)
[Warning][Deadcode][CWE-570] condition '_hj_k == 8U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1480-996:1486)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:2820-999:2822)
[Warning][Deadcode][CWE-570] condition '_hj_k == 7U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1529-996:1535)
[Warning][Deadcode][CWE-570] condition '_hj_k == 6U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1578-996:1584)
[Warning][Deadcode][CWE-570] condition '_hj_k == 11U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1319-996:1326)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:998:8-998:23)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:935:54-935:55)
[Warning][Deadcode][CWE-570] condition '_hj_k == 5U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1626-996:1632)
[Warning][Deadcode][CWE-570] condition '_hj_k == 10U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1374-996:1381)
[Warning][Deadcode][CWE-571] condition '_hj_k == 4U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1655-996:1661)
[Warning][Deadcode][CWE-570] condition '_hj_k == 9U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1428-996:1434)
[Warning][Deadcode][CWE-570] condition '! user->hh.tbl' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:2747-996:2762)
[Warning][Deadcode][CWE-570] condition '_hj_k == 8U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1480-996:1486)
[Warning][Deadcode][CWE-570] condition '_hj_k == 7U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1529-996:1535)
[Warning][Deadcode][CWE-570] condition '_hj_k == 6U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1578-996:1584)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:1349-1001:1351)
[Warning][Deadcode][CWE-570] condition '_hj_k == 5U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1626-996:1632)
[Warning][Deadcode][CWE-571] condition '_hj_k == 4U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:1655-996:1661)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 >= 12U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:223-999:235)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:6105-996:6107)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 11U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1308-999:1315)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 10U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1363-999:1370)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:3173-999:3175)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 9U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1417-999:1423)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:6120-996:6122)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3325-996:3327)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:3250-999:3252)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 8U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1469-999:1475)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:6137-996:6139)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 7U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1518-999:1524)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:3220-999:3222)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 6U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1567-999:1573)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:6152-996:6154)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:3237-999:3239)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 5U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1615-999:1621)
[Warning][Deadcode][CWE-571] condition '_hj_k___0 == 4U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1644-999:1650)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3602-996:3604)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:989:8-989:23)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:1001:703-1001:705)
[Warning][Deadcode][CWE-570] condition '(unsigned int )user == (unsigned int )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:991:13-991:32)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:996:3740-996:3742)
[Warning][Deadcode][CWE-570] condition '(unsigned int )user == (unsigned int )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:991:13-991:32)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 11U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test6-1.i:999:1308-999:1315)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
