./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_test1-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_test1-1.i:757:2670-757:3297 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3360-757:3574 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3631-757:3712 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4976-757:5072 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:5-761:5 with factor 12
[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] 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_test1-1.i:757:4981-757:5059)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4981-757:5059)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5190-757:5226)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5232-757:5318)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5322-757:5347)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Info][Unsound] Unknown address in {&(alloc@sid:153).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Info][Unsound] Unknown address in {&(alloc@sid:153)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:153).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {?, NULL, &(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Info][Unsound] Unknown address in {&(alloc@sid:648)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[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_test1-1.i:757:1663-757:1702)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1663-757: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_test1-1.i:757:1712-757:1751)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1712-757: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_test1-1.i:757:1761-757:1799)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1761-757:1799)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1809-757:1828)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1837-757:1851)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1853-757:1871)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1903-757:1921)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1923-757:1937)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1939-757:1962)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1964-757:1982)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1984-757: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_test1-1.i:757:2004-757:2032)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2034-757:2048)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2050-757: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_test1-1.i:757:2070-757:2098)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2100-757:2118)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2120-757:2134)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2136-757:2160)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2162-757:2180)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2182-757: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_test1-1.i:757:2202-757:2229)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2231-757:2245)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2247-757: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_test1-1.i:757:2267-757:2294)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2296-757:2314)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2316-757:2330)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2332-757:2356)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2358-757:2376)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2378-757: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_test1-1.i:757:2398-757:2426)
[Info][Unsound] Unknown address in {&(alloc@sid:153).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Info][Unsound] Unknown address in {&(alloc@sid:648)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Info][Unsound] Unknown address in {&(alloc@sid:153)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:153).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {?, NULL, &(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:153).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {?, NULL, &(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Info][Unsound] Unknown address in {&(alloc@sid:153)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Info][Unsound] Unknown address in {&(alloc@sid:153).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:153).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {?, NULL, &(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Info][Unsound] Unknown address in {&(alloc@sid:648)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Info][Unsound] Unknown address in {&(alloc@sid:153).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Info][Unsound] Unknown address in {&(alloc@sid:153)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:153).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {?, NULL, &(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Info][Unsound] Unknown address in {&(alloc@sid:648)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Info][Unsound] Unknown address in {&(alloc@sid:153).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2676-757:2737)
[Info][Unsound] Unknown address in {&(alloc@sid:648)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2676-757:2737)
[Info][Unsound] Unknown address in {&(alloc@sid:153)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2676-757:2737)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:153).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {?, NULL, &(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2676-757:2737)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2676-757:2737)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2676-757:2737)
[Info][Unsound] Unknown address in {&(alloc@sid:153).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2833-757:2868)
[Info][Unsound] Unknown address in {&(alloc@sid:153)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2833-757:2868)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:153).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {?, NULL, &(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2833-757:2868)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2833-757:2868)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2833-757:2868)
[Info][Unsound] Unknown address in {&(alloc@sid:648)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2833-757:2868)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2945-757:3002)
[Info][Unsound] Unknown address in {&(alloc@sid:153).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3005-757:3090)
[Info][Unsound] Unknown address in {&(alloc@sid:153)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3005-757:3090)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:153).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {?, NULL, &(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3005-757:3090)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3005-757:3090)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3005-757:3090)
[Info][Unsound] Unknown address in {&(alloc@sid:648)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3005-757:3090)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3206-757:3278)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3602-757:3629)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3636-757:3699)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3784-757:3801)
[Info][Unsound] Unknown address in {&(alloc@sid:153).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Info][Unsound] Unknown address in {&(alloc@sid:153)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:153).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {?, NULL, &(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Info][Unsound] Unknown address in {&(alloc@sid:648)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4011-757:4100)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4011-757:4100)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4238-757:4352)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4501-757:4724)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4501-757:4724)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4501-757:4724)
[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_test1-1.i:757:4501-757:4724)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5605-757:5642)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5646-757:5684)
[Info][Unsound] Unknown address in {&(alloc@sid:648)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Info][Unsound] Unknown address in {&(alloc@sid:153).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Info][Unsound] Unknown address in {&(alloc@sid:153)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:153).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {?, NULL, &(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[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_test1-1.i:757:5737-757:5900)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5737-757:5900)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:708:11-708:26)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-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_test1-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_test1-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_test1-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_test1-1.i:302:1-306:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:753-753)
[Warning][Deadcode] Function 'reach_error' has dead code:
  on line 700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:700-700)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 40
  dead: 7 (5 in uncalled functions)
  total lines: 47
[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_test1-1.i:757:6003-757:6005)
[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_test1-1.i:757:6018-757:6020)
[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_test1-1.i:757:6035-757:6037)
[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_test1-1.i:757:3295-757:3297)
[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_test1-1.i:757:6050-757:6052)
[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_test1-1.i:757:6063-757:6065)
[Warning][Deadcode][CWE-570] condition '_hj_k == 11U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1319-757: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_test1-1.i:757:1374-757: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_test1-1.i:757:1428-757: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_test1-1.i:757:1480-757: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_test1-1.i:757:1529-757: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_test1-1.i:757:1578-757:1584)
[Warning][Deadcode][CWE-570] condition '_hj_k == 5U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1626-757: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_test1-1.i:757:1655-757:1661)
[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_test1-1.i:757:3710-757:3712)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:699:54-699:55)
[Warning][Deadcode][CWE-570] condition '! _he_new_buckets' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4358-757:4374)
[Warning][Deadcode][CWE-570] condition '(unsigned long )user == (unsigned long )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:752:13-752: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_test1-1.i:757:5070-757:5072)
[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_test1-1.i:757:2437-757: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_test1-1.i:757:3572-757:3574)
[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_test1-1.i:757:2450-757:2452)
[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_test1-1.i:757:234-757: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_test1-1.i:757:2463-757:2465)
[Warning][Deadcode][CWE-570] condition '! user->hh.tbl' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2743-757:2758)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
