./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_test7-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_test7-1.i:722:2670-722:3297 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3360-722:3574 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3631-722:3712 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:4976-722:5072 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2513-725:2594 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2685-725:2822 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:3062-725:3171 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:551-727:614 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:762-727:851 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:853-727:1213 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:733:5-735: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_test7-1.i:722:4981-722:5059)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:4981-722:5059)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5120-722:5184)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5190-722:5226)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5232-722:5318)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5322-722:5347)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5467-722:5505)
[Info][Unsound] Unknown address in {&(alloc@sid:26).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5509-722:5538)
[Info][Unsound] Unknown address in {&(alloc@sid:26)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5509-722:5538)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:26).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:26).hh}
                                                       key -> {&(alloc@sid:26).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:26)}
                                                       prev -> {?, NULL, &(alloc@sid:26).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:198)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5509-722:5538)
[Info][Unsound] Unknown value in {&(alloc@sid:26).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_test7-1.i:722:5509-722: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_test7-1.i:722:5509-722:5538)
[Info][Unsound] Unknown address in {&(alloc@sid:521)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5509-722: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_test7-1.i:722:1663-722:1702)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:1663-722: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_test7-1.i:722:1712-722:1751)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:1712-722: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_test7-1.i:722:1761-722:1799)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:1761-722:1799)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:1809-722:1828)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:1837-722:1851)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:1853-722:1871)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:1903-722:1921)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:1923-722:1937)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:1939-722:1962)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:1964-722:1982)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:1984-722: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_test7-1.i:722:2004-722:2032)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2034-722:2048)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2050-722: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_test7-1.i:722:2070-722:2098)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2100-722:2118)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2120-722:2134)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2136-722:2160)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2162-722:2180)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2182-722: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_test7-1.i:722:2202-722:2229)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2231-722:2245)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2247-722: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_test7-1.i:722:2267-722:2294)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2296-722:2314)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2316-722:2330)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2332-722:2356)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2358-722:2376)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2378-722: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_test7-1.i:722:2398-722:2426)
[Info][Unsound] Unknown address in {&(alloc@sid:26).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3327-722:3358)
[Info][Unsound] Unknown address in {&(alloc@sid:521)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3327-722:3358)
[Info][Unsound] Unknown address in {&(alloc@sid:26)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3327-722:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:26).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:26).hh}
                                                       key -> {&(alloc@sid:26).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:26)}
                                                       prev -> {?, NULL, &(alloc@sid:26).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:198)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3327-722:3358)
[Info][Unsound] Unknown value in {&(alloc@sid:26).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_test7-1.i:722:3327-722: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_test7-1.i:722:3327-722:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:26).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:26).hh}
                                                       key -> {&(alloc@sid:26).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:26)}
                                                       prev -> {?, NULL, &(alloc@sid:26).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:198)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3397-722:3484)
[Info][Unsound] Unknown value in {&(alloc@sid:26).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_test7-1.i:722:3397-722:3484)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3487-722:3522)
[Info][Unsound] Unknown address in {&(alloc@sid:26)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3487-722:3522)
[Info][Unsound] Unknown address in {&(alloc@sid:26).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3487-722:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:26).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:26).hh}
                                                       key -> {&(alloc@sid:26).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:26)}
                                                       prev -> {?, NULL, &(alloc@sid:26).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:198)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3487-722:3522)
[Info][Unsound] Unknown value in {&(alloc@sid:26).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_test7-1.i:722:3487-722: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_test7-1.i:722:3487-722:3522)
[Info][Unsound] Unknown address in {&(alloc@sid:521)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3487-722:3522)
[Info][Unsound] Unknown address in {&(alloc@sid:26).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3525-722:3561)
[Info][Unsound] Unknown address in {&(alloc@sid:26)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3525-722:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:26).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:26).hh}
                                                       key -> {&(alloc@sid:26).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:26)}
                                                       prev -> {?, NULL, &(alloc@sid:26).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:198)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3525-722:3561)
[Info][Unsound] Unknown value in {&(alloc@sid:26).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_test7-1.i:722:3525-722: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_test7-1.i:722:3525-722:3561)
[Info][Unsound] Unknown address in {&(alloc@sid:521)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3525-722:3561)
[Info][Unsound] Unknown address in {&(alloc@sid:26).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2676-722:2737)
[Info][Unsound] Unknown address in {&(alloc@sid:521)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2676-722:2737)
[Info][Unsound] Unknown address in {&(alloc@sid:26)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2676-722:2737)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:26).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:26).hh}
                                                       key -> {&(alloc@sid:26).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:26)}
                                                       prev -> {?, NULL, &(alloc@sid:26).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:198)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2676-722:2737)
[Info][Unsound] Unknown value in {&(alloc@sid:26).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_test7-1.i:722:2676-722: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_test7-1.i:722:2676-722:2737)
[Info][Unsound] Unknown address in {&(alloc@sid:26).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2833-722:2868)
[Info][Unsound] Unknown address in {&(alloc@sid:26)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2833-722:2868)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:26).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:26).hh}
                                                       key -> {&(alloc@sid:26).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:26)}
                                                       prev -> {?, NULL, &(alloc@sid:26).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:198)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2833-722:2868)
[Info][Unsound] Unknown value in {&(alloc@sid:26).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_test7-1.i:722:2833-722: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_test7-1.i:722:2833-722:2868)
[Info][Unsound] Unknown address in {&(alloc@sid:521)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2833-722: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_test7-1.i:722:2945-722:3002)
[Info][Unsound] Unknown address in {&(alloc@sid:26).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3005-722:3090)
[Info][Unsound] Unknown address in {&(alloc@sid:26)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3005-722:3090)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:26).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:26).hh}
                                                       key -> {&(alloc@sid:26).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:26)}
                                                       prev -> {?, NULL, &(alloc@sid:26).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:198)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3005-722:3090)
[Info][Unsound] Unknown value in {&(alloc@sid:26).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_test7-1.i:722:3005-722: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_test7-1.i:722:3005-722:3090)
[Info][Unsound] Unknown address in {&(alloc@sid:521)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3005-722:3090)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3206-722:3278)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3602-722:3629)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3636-722:3699)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3784-722:3801)
[Info][Unsound] Unknown address in {&(alloc@sid:26).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3804-722:3845)
[Info][Unsound] Unknown address in {&(alloc@sid:26)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3804-722:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:26).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:26).hh}
                                                       key -> {&(alloc@sid:26).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:26)}
                                                       prev -> {?, NULL, &(alloc@sid:26).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:198)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3804-722:3845)
[Info][Unsound] Unknown value in {&(alloc@sid:26).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_test7-1.i:722:3804-722: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_test7-1.i:722:3804-722:3845)
[Info][Unsound] Unknown address in {&(alloc@sid:521)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3804-722:3845)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:3925-722:3967)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:4011-722:4100)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:4011-722:4100)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:4238-722:4352)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:4501-722:4724)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:4501-722:4724)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:4501-722: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_test7-1.i:722:4501-722:4724)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5605-722:5642)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5646-722:5684)
[Info][Unsound] Unknown address in {&(alloc@sid:521)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5688-722:5733)
[Info][Unsound] Unknown address in {&(alloc@sid:26).hh} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5688-722: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_test7-1.i:722:5688-722:5733)
[Info][Unsound] Unknown address in {&(alloc@sid:26)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5688-722:5733)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {?, NULL, &(alloc@sid:26).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:26).hh}
                                                       key -> {&(alloc@sid:26).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:26)}
                                                       prev -> {?, NULL, &(alloc@sid:26).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:198)}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5688-722:5733)
[Info][Unsound] Unknown value in {&(alloc@sid:26).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_test7-1.i:722:5688-722: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_test7-1.i:722:5737-722:5900)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:5737-722:5900)
[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_test7-1.i:725:3068-725:3158)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]),[0,999],not {} ([-31,31]))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1652-725:1691)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1652-725:1691)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]),[0,999],not {} ([-31,31]))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1701-725:1740)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1701-725:1740)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]),[0,999],not {} ([-31,31]))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1750-725:1788)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1750-725:1788)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1798-725:1817)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1826-725:1840)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1842-725:1860)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1892-725:1910)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1912-725:1926)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1928-725:1951)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1953-725:1971)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:1973-725: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_test7-1.i:725:1993-725:2021)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2023-725:2037)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2039-725: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_test7-1.i:725:2059-725:2087)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2089-725:2107)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2109-725:2123)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2125-725:2149)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2151-725:2169)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2171-725: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_test7-1.i:725:2191-725:2218)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2220-725:2234)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2236-725: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_test7-1.i:725:2256-725:2283)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2285-725:2303)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2305-725:2319)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2321-725:2345)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2347-725:2365)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2367-725: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_test7-1.i:725:2387-725: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_test7-1.i:725:2518-725:2581)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2518-725: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_test7-1.i:725:2623-725: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_test7-1.i:725:2691-725:2809)
[Info][Imprecise] Invalidating expressions: & tmp___5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2966-725:3007)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:257-727: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_test7-1.i:727:257-727:292)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:297-727:396)
[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_test7-1.i:727:297-727:396)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:440-727:540)
[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_test7-1.i:727:440-727:540)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:658-727:758)
[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_test7-1.i:727:658-727:758)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:767-727:838)
[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_test7-1.i:727:767-727:838)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:767-727:838)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:873-727:921)
[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_test7-1.i:727:873-727:921)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:923-727:940)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:1058-727:1111)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:1145-727:1198)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:1216-727:1243)
[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_test7-1.i:727:1216-727:1243)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:1216-727:1243)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:148-727:178)
[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_test7-1.i:727:148-727:178)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)(users->hh.tbl)->buckets in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:148-727:178)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:727:180-727:201)
[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_test7-1.i:727:180-727:201)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Pointer (void *)users->hh.tbl 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_test7-1.i:727:180-727:201)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)tmp in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:728:13-728:22)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-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_test7-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_test7-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_test7-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_test7-1.i:302:1-306:1)
[Warning][Deadcode] Function '__VERIFIER_assert' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:701:1-705:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:718-718)
[Warning][Deadcode] Function 'reach_error' has dead code:
  on line 700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:700-700)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 19
  dead: 10 (8 in uncalled functions)
  total lines: 29
[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_test7-1.i:722:6003-722: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_test7-1.i:727:612-727:614)
[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_test7-1.i:722:6018-722: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_test7-1.i:722:6035-722: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_test7-1.i:722:3295-722: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_test7-1.i:722:6050-722: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_test7-1.i:727:849-727:851)
[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_test7-1.i:722:6063-722: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_test7-1.i:722:1319-722: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_test7-1.i:722:1374-722: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_test7-1.i:722:1428-722: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_test7-1.i:722:1480-722: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_test7-1.i:722:1529-722: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_test7-1.i:722:1578-722: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_test7-1.i:722:1626-722:1632)
[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_test7-1.i:727:1211-727:1213)
[Warning][Deadcode][CWE-571] condition '_hj_k == 4U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:1655-722: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_test7-1.i:722:3710-722:3712)
[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_test7-1.i:725:2426-725: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_test7-1.i:725:2439-725:2441)
[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_test7-1.i:725:223-725: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_test7-1.i:725:2452-725:2454)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-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_test7-1.i:722:4358-722:4374)
[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_test7-1.i:725:2592-725:2594)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:725:2601-725: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_test7-1.i:725:2820-725:2822)
[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_test7-1.i:717:13-717: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_test7-1.i:722:5070-722:5072)
[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_test7-1.i:725:1308-725: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_test7-1.i:725:1363-725: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_test7-1.i:725:3169-725:3171)
[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_test7-1.i:722:2437-722:2439)
[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_test7-1.i:725:1417-725: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_test7-1.i:722:3572-722:3574)
[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_test7-1.i:725:1469-725: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_test7-1.i:722:2450-722: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_test7-1.i:722:234-722:246)
[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_test7-1.i:725:1518-725: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_test7-1.i:725:3216-725:3218)
[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_test7-1.i:722:2463-722:2465)
[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_test7-1.i:725:1567-725:1573)
[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_test7-1.i:725:1615-725:1621)
[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_test7-1.i:725:3233-725:3235)
[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_test7-1.i:725:1644-725: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_test7-1.i:725:3246-725:3248)
[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_test7-1.i:727:1258-727:1260)
[Warning][Deadcode][CWE-570] condition '! user->hh.tbl' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test7-1.i:722:2743-722:2758)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
