./goblint --conf conf/examples/large-program.json --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --disable witness.graphml.enabled --set 'lib.activated[+]' zlib --set 'lib.activated[+]' pcre --set 'lib.activated[+]' liblzma --sets ana.specification /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c


--------------------------------------------------------------------------------


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
Option warning: ana.base.context.int implicitly disabled by ana.base.context.non-ptr
Option warning: ana.base.context.interval implicitly disabled by ana.base.context.int
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(pthread_rwlock_t, TComp(union __anonunion_pthread_rwlock_t_656928968, __data : TComp(struct __pthread_rwlock_arch_t, __readers : TInt(unsigned int, ), __writers : TInt(unsigned int, ), __wrphase_futex : TInt(unsigned int, ), __writers_futex : TInt(unsigned int, ), __pad3 : TInt(unsigned int, ), __pad4 : TInt(unsigned int, ), __cur_writer : TInt(int, ), __shared : TInt(int, ), __rwelision : TInt(signed char, ), __pad1 : TArray(TInt(unsigned char, ), Some(Const(Int(7,int,7))), ), __pad2 : TInt(unsigned long, ), __flags : TInt(unsigned int, ), , ), __size : TArray(TInt(char, ), Some(Const(Int(56,int,56))), ), __align : TInt(long, ), , ), ),  __restrict  ), AddrOf(Var(lock, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:772:3-772:129)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:772:3-772:129)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TComp(struct _IO_FILE, _flags : TInt(int, ), _IO_read_ptr : TPtr(TInt(char, ), ), _IO_read_end : TPtr(TInt(char, ), ), _IO_read_base : TPtr(TInt(char, ), ), _IO_write_base : TPtr(TInt(char, ), ), _IO_write_ptr : TPtr(TInt(char, ), ), _IO_write_end : TPtr(TInt(char, ), ), _IO_buf_base : TPtr(TInt(char, ), ), _IO_buf_end : TPtr(TInt(char, ), ), _IO_save_base : TPtr(TInt(char, ), ), _IO_backup_base : TPtr(TInt(char, ), ), _IO_save_end : TPtr(TInt(char, ), ), _markers : TPtr(TComp(struct _IO_marker, , , ), ), _chain : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _fileno : TInt(int, ), _flags2 : TInt(int, ), _old_offset : TNamed(__off_t, TInt(long, ), ), _cur_column : TInt(unsigned short, ), _vtable_offset : TInt(signed char, ), _shortbuf : TArray(TInt(char, ), Some(Const(Int(1,int,1))), ), _lock : TPtr(TNamed(_IO_lock_t, TVoid(), ), ), _offset : TNamed(__off64_t, TInt(long, ), ), _codecvt : TPtr(TComp(struct _IO_codecvt, , , ), ), _wide_data : TPtr(TComp(struct _IO_wide_data, , , ), ), _freeres_list : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _freeres_buf : TPtr(TVoid(), ), __pad5 : TNamed(size_t, TInt(unsigned long, ), ), _mode : TInt(int, ), _unused2 : TArray(TInt(char, ), Some(MinusA(MinusA(*(Const(Int(f,unsigned long,15UL)), sizeof(TInt(int, ))), *(Const(Int(4,unsigned long,4UL)), sizeof(TPtr(TVoid(), )))), sizeof(TNamed(size_t, TInt(unsigned long, ), )))), ), , ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:774:5-774:88)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:774:5-774:88)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:774:5-774:88)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:774:5-774:88)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:777:3-778:79)
[Warning][Imprecise] Trying to update an index, but was not given an array({
                                                        hashv -> (Unknown int([0,32]))
                                                        hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                        hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                        key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                        keylen -> (4)
                                                        next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                        prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                        tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                      }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:290:23-290:67)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:290:23-290:67)
[Warning][Imprecise] Trying to update an index, but was not given an array({
                                                        hashv -> (Unknown int([0,32]))
                                                        hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                        hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                        key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                        keylen -> (4)
                                                        next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                        prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                        tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                      }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:289:21-289:45)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:289:21-289:45)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:297:21-297:81)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:299:21-299:87)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:299:21-299:87)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:160:5-160:40)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:229:13-229:57)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:231:13-231:57)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:233:13-233:56)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:276:15-276:71)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:280:19-280:110)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:280:19-280:110)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:282:19-282:116)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:282:19-282:116)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:291:21-291:83)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:291:21-291:83)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:783:3-784:79)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:789:3-790:79)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:701:27-701:56)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:703:29-703:92)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:714:27-714:82)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:715:27-715:65)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:717:30-717:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:717:30-717:69)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top)).hh} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:719:27-719:56)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:719:27-719:56)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> (Unknown int([0,32]))
                                                       hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                       keylen -> (4)
                                                       next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                       prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                       tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                     }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:719:27-719:56)
[Info][Unsound] Unknown value in {&(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:719:27-719:56)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:719:27-719:56)
[Info][Unsound] Unknown address in {&(alloc@sid:749@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:719:27-719:56)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:699:25-699:78)
[Warning][Imprecise] Trying to update an index, but was not given an array({
                                                        hashv -> (Unknown int([0,32]))
                                                        hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                        hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                        key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                        keylen -> (4)
                                                        next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                        prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                        tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                      }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:489:23-489:67)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:489:23-489:67)
[Warning][Imprecise] Trying to update an index, but was not given an array({
                                                        hashv -> (Unknown int([0,32]))
                                                        hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                        hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                        key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                        keylen -> (4)
                                                        next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                        prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                        tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                      }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:488:21-488:45)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:488:21-488:45)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:496:21-496:81)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:498:21-498:87)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:498:21-498:87)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:359:5-359:40)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:428:13-428:57)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:430:13-430:57)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:432:13-432:56)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:475:15-475:71)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:479:19-479:110)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:479:19-479:110)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:481:19-481:116)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:481:19-481:116)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:490:21-490:83)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:490:21-490:83)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:582:13-582:65)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:584:13-584:65)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:586:13-586:64)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:657:13-657:37)
[Info][Unsound] Unknown address in {&(alloc@sid:749@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:657:13-657:37)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top)).hh} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:657:13-657:37)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:657:13-657:37)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> (Unknown int([0,32]))
                                                       hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                       keylen -> (4)
                                                       next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                       prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                       tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                     }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:657:13-657:37)
[Info][Unsound] Unknown value in {&(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:657:13-657:37)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:657:13-657:37)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:660:15-660:88)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> (Unknown int([0,32]))
                                                       hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                       keylen -> (4)
                                                       next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                       prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                       tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                     }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:660:15-660:88)
[Info][Unsound] Unknown value in {&(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:660:15-660:88)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:661:17-661:55)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:661:17-661:55)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top)).hh} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:661:17-661:55)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> (Unknown int([0,32]))
                                                       hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                       keylen -> (4)
                                                       next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                       prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                       tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                     }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:661:17-661:55)
[Info][Unsound] Unknown value in {&(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:661:17-661:55)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:661:17-661:55)
[Info][Unsound] Unknown address in {&(alloc@sid:749@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:661:17-661:55)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:662:16-662:45)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top)).hh} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:662:16-662:45)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:662:16-662:45)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> (Unknown int([0,32]))
                                                       hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                       keylen -> (4)
                                                       next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                       prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                       tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                     }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:662:16-662:45)
[Info][Unsound] Unknown value in {&(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:662:16-662:45)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:662:16-662:45)
[Info][Unsound] Unknown address in {&(alloc@sid:749@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:662:16-662:45)
[Info][Unsound] Unknown address in {&(alloc@sid:749@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:634:15-634:51)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top)).hh} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:634:15-634:51)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:634:15-634:51)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> (Unknown int([0,32]))
                                                       hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                       keylen -> (4)
                                                       next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                       prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                       tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                     }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:634:15-634:51)
[Info][Unsound] Unknown value in {&(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:634:15-634:51)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:634:15-634:51)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top)).hh} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:639:18-639:44)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:639:18-639:44)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> (Unknown int([0,32]))
                                                       hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                       keylen -> (4)
                                                       next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                       prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                       tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                     }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:639:18-639:44)
[Info][Unsound] Unknown value in {&(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:639:18-639:44)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:639:18-639:44)
[Info][Unsound] Unknown address in {&(alloc@sid:749@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:639:18-639:44)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top)).hh} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:644:18-644:65)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:644:18-644:65)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> (Unknown int([0,32]))
                                                       hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                       keylen -> (4)
                                                       next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                       prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                       tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                     }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:644:18-644:65)
[Info][Unsound] Unknown value in {&(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:644:18-644:65)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:644:18-644:65)
[Info][Unsound] Unknown address in {&(alloc@sid:749@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:644:18-644:65)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:650:19-650:102)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:655:13-655:21)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top)).hh} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:655:13-655:21)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> (Unknown int([0,32]))
                                                       hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                       keylen -> (4)
                                                       next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                       prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                       tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                     }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:655:13-655:21)
[Info][Unsound] Unknown value in {&(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:655:13-655:21)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:655:13-655:21)
[Info][Unsound] Unknown address in {&(alloc@sid:749@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:655:13-655:21)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:667:15-667:43)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:669:15-669:71)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:673:15-673:59)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:674:16-674:35)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top)).hh} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:675:15-675:48)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:675:15-675:48)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> (Unknown int([0,32]))
                                                       hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                       keylen -> (4)
                                                       next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                       prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                       tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                     }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:675:15-675:48)
[Info][Unsound] Unknown value in {&(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:675:15-675:48)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:675:15-675:48)
[Info][Unsound] Unknown address in {&(alloc@sid:749@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:675:15-675:48)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:675:15-675:48)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:677:19-677:83)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:678:18-678:55)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:678:18-678:55)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:680:15-680:42)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:681:19-681:72)
[Info][Unsound] Unknown address in {&(alloc@sid:749@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:727:24-727:61)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top)).hh} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:727:24-727:61)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:727:24-727:61)
[Info][Unsound] Unknown address in {&(alloc@sid:488@tid:Top Threads(#top))} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:727:24-727:61)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> (Unknown int([0,32]))
                                                       hh_next -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       hh_prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh}
                                                       key -> {&(alloc@sid:488@tid:Top Threads(#top)).i}
                                                       keylen -> (4)
                                                       next -> {NULL, &(alloc@sid:488@tid:Top Threads(#top))}
                                                       prev -> {?, NULL, &(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]}
                                                       tbl -> {&(alloc@sid:672@tid:Top Threads(#top))}
                                                     }) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:727:24-727:61)
[Info][Unsound] Unknown value in {&(alloc@sid:488@tid:Top Threads(#top)).hh[def_exc:Unknown int([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:727:24-727:61)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TComp(struct _IO_FILE, _flags : TInt(int, ), _IO_read_ptr : TPtr(TInt(char, ), ), _IO_read_end : TPtr(TInt(char, ), ), _IO_read_base : TPtr(TInt(char, ), ), _IO_write_base : TPtr(TInt(char, ), ), _IO_write_ptr : TPtr(TInt(char, ), ), _IO_write_end : TPtr(TInt(char, ), ), _IO_buf_base : TPtr(TInt(char, ), ), _IO_buf_end : TPtr(TInt(char, ), ), _IO_save_base : TPtr(TInt(char, ), ), _IO_backup_base : TPtr(TInt(char, ), ), _IO_save_end : TPtr(TInt(char, ), ), _markers : TPtr(TComp(struct _IO_marker, , , ), ), _chain : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _fileno : TInt(int, ), _flags2 : TInt(int, ), _old_offset : TNamed(__off_t, TInt(long, ), ), _cur_column : TInt(unsigned short, ), _vtable_offset : TInt(signed char, ), _shortbuf : TArray(TInt(char, ), Some(Const(Int(1,int,1))), ), _lock : TPtr(TNamed(_IO_lock_t, TVoid(), ), ), _offset : TNamed(__off64_t, TInt(long, ), ), _codecvt : TPtr(TComp(struct _IO_codecvt, , , ), ), _wide_data : TPtr(TComp(struct _IO_wide_data, , , ), ), _freeres_list : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _freeres_buf : TPtr(TVoid(), ), __pad5 : TNamed(size_t, TInt(unsigned long, ), ), _mode : TInt(int, ), _unused2 : TArray(TInt(char, ), Some(MinusA(MinusA(*(Const(Int(f,unsigned long,15UL)), sizeof(TInt(int, ))), *(Const(Int(4,unsigned long,4UL)), sizeof(TPtr(TVoid(), )))), sizeof(TNamed(size_t, TInt(unsigned long, ), )))), ), , ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:735:25-735:127)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:735:25-735:127)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:735:25-735:127)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:735:25-735:127)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:795:3-796:79)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(thread_result, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:801:3-801:52)
[Info][Unsound] Unknown address in {&thread_result} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:801:3-801:52)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:801:3-801:52)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:801:3-801:52)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(thread_result, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:803:3-803:52)
[Info][Unsound] Unknown address in {&thread_result} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:803:3-803:52)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:803:3-803:52)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:803:3-803:52)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(thread_result, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:805:3-805:52)
[Info][Unsound] Unknown address in {&thread_result} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:805:3-805:52)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:805:3-805:52)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:805:3-805:52)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(thread_result, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:807:3-807:52)
[Info][Unsound] Unknown address in {&thread_result} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:807:3-807:52)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:807:3-807:52)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:807:3-807:52)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:810:5-810:34)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___1, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:815:3-815:43)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TComp(struct _IO_FILE, _flags : TInt(int, ), _IO_read_ptr : TPtr(TInt(char, ), ), _IO_read_end : TPtr(TInt(char, ), ), _IO_read_base : TPtr(TInt(char, ), ), _IO_write_base : TPtr(TInt(char, ), ), _IO_write_ptr : TPtr(TInt(char, ), ), _IO_write_end : TPtr(TInt(char, ), ), _IO_buf_base : TPtr(TInt(char, ), ), _IO_buf_end : TPtr(TInt(char, ), ), _IO_save_base : TPtr(TInt(char, ), ), _IO_backup_base : TPtr(TInt(char, ), ), _IO_save_end : TPtr(TInt(char, ), ), _markers : TPtr(TComp(struct _IO_marker, , , ), ), _chain : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _fileno : TInt(int, ), _flags2 : TInt(int, ), _old_offset : TNamed(__off_t, TInt(long, ), ), _cur_column : TInt(unsigned short, ), _vtable_offset : TInt(signed char, ), _shortbuf : TArray(TInt(char, ), Some(Const(Int(1,int,1))), ), _lock : TPtr(TNamed(_IO_lock_t, TVoid(), ), ), _offset : TNamed(__off64_t, TInt(long, ), ), _codecvt : TPtr(TComp(struct _IO_codecvt, , , ), ), _wide_data : TPtr(TComp(struct _IO_wide_data, , , ), ), _freeres_list : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _freeres_buf : TPtr(TVoid(), ), __pad5 : TNamed(size_t, TInt(unsigned long, ), ), _mode : TInt(int, ), _unused2 : TArray(TInt(char, ), Some(MinusA(MinusA(*(Const(Int(f,unsigned long,15UL)), sizeof(TInt(int, ))), *(Const(Int(4,unsigned long,4UL)), sizeof(TPtr(TVoid(), )))), sizeof(TNamed(size_t, TInt(unsigned long, ), )))), ), , ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:817:5-817:91)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:817:5-817:91)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:817:5-817:91)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:817:5-817:91)
[Warning][Deadcode] Function 'thread_routine_r' has dead code:
  on lines 162..163 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:162-163)
  on lines 176..206 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:176-206)
  on lines 209..210 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:209-210)
  on line 215 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:215-215)
  on line 217 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:217-217)
  on line 219 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:219-219)
  on line 221 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:221-221)
  on line 223 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:223-223)
  on line 225 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:225-225)
  on line 227 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:227-227)
  on line 230 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:230-230)
  on line 232 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:232-232)
  on line 234 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:234-234)
[Warning][Deadcode] Function 'thread_routine_w' has dead code:
  on lines 361..362 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:361-362)
  on lines 375..405 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:375-405)
  on lines 408..409 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:408-409)
  on line 414 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:414-414)
  on line 416 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:416-416)
  on line 418 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:418-418)
  on line 420 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:420-420)
  on line 422 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:422-422)
  on line 424 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:424-424)
  on line 426 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:426-426)
  on line 429 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:429-429)
  on line 431 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:431-431)
  on line 433 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:433-433)
  on line 517 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:517-517)
  on lines 529..559 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:529-559)
  on lines 562..563 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:562-563)
  on line 568 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:568-568)
  on line 570 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:570-570)
  on line 572 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:572-572)
  on line 574 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:574-574)
  on line 576 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:576-576)
  on line 578 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:578-578)
  on line 580 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:580-580)
  on line 583 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:583-583)
  on line 585 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:585-585)
  on line 587 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:587-587)
  on line 636 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:636-636)
  on line 648 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:648-648)
  on line 687 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:687-687)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 339
  dead: 137
  total lines: 476
[Warning][Deadcode][CWE-570] condition '_hj_k == 11U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:413:13-413:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:668:20-668:21)
[Warning][Deadcode][CWE-570] condition '_hj_k == 10U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:415:13-415:21)
[Warning][Deadcode][CWE-570] condition '_hj_k == 9U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:417:13-417:20)
[Warning][Deadcode][CWE-570] condition '_hj_k == 8U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:419:13-419:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:497:26-497:27)
[Warning][Deadcode][CWE-570] condition '_hj_k == 7U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:421:13-421:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:672:20-672:21)
[Warning][Deadcode][CWE-570] condition '_hj_k == 11U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:214:13-214:21)
[Warning][Deadcode][CWE-570] condition '_hj_k == 6U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:423:13-423:20)
[Warning][Deadcode][CWE-570] condition '_hj_k == 10U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:216:13-216:21)
[Warning][Deadcode][CWE-570] condition '_hj_k == 5U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:425:13-425:20)
[Warning][Deadcode][CWE-570] condition '_hj_k == 9U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:218:13-218:20)
[Warning][Deadcode][CWE-571] condition '_hj_k == 4U' is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:427:13-427:20)
[Warning][Deadcode][CWE-570] condition '_hj_k == 8U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:220:13-220:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:298:26-298:27)
[Warning][Deadcode][CWE-570] condition '_hj_k == 7U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:222:13-222:20)
[Warning][Deadcode][CWE-570] condition '_hj_k == 6U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:224:13-224:20)
[Warning][Deadcode][CWE-570] condition '_hj_k == 5U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:226:13-226:20)
[Warning][Deadcode][CWE-571] condition '_hj_k == 4U' is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:228:13-228:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:591:20-591:21)
[Warning][Deadcode][CWE-570] condition '! e' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:516:11-516:14)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:683:26-683:27)
[Warning][Deadcode][CWE-570] condition '! _he_new_buckets' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:686:25-686:42)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:520:14-520:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:521:16-521:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:522:18-522:19)
[Warning][Deadcode][CWE-570] condition 'tmp != 0' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:360:9-360:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:437:20-437:21)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 >= 12U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:528:20-528:36)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:364:12-364:13)
[Warning][Deadcode][CWE-570] condition 'tmp != 0' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:161:9-161:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:238:20-238:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:702:34-702:35)
[Warning][Race] Memory location elts (race with conf. 110): (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:140:5-140:31)
  write with lock:{lock} (conf. 110)  (exp: & elts) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:655:13-655:21)
  read with [] (conf. 110)  (exp: & elts) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:809:7-809:58)
  read with [] (conf. 110)  (exp: & elts) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:810:5-810:34)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:367:16-367:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:625:16-625:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:165:12-165:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:368:18-368:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:168:16-168:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:632:20-632:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:169:18-169:19)
[Warning][Deadcode][CWE-570] condition '_hj_k >= 12U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:374:20-374:32)
[Warning][Deadcode][CWE-570] condition '! e->hh.tbl' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:635:19-635:30)
[Warning][Race] Memory location (alloc@sid:672@tid:Top Threads(#top)).num_items (race with conf. 110): (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:633:15-633:55)
  write with lock:{lock} (conf. 110)  (exp: (void *)e->hh.tbl) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:638:17-638:74)
  write with lock:{lock} (conf. 110)  (exp: & (elts->hh.tbl)->num_items) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:667:15-667:43)
  read with [] (conf. 110)  (exp: & (elts->hh.tbl)->num_items) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:810:5-810:34)
[Warning][Deadcode][CWE-570] condition '_hj_k >= 12U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:175:20-175:32)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:471:16-471:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:474:20-474:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:272:16-272:17)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 11U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:567:13-567:21)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 10U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:569:13-569:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:478:20-478:21)
[Warning][Race] Memory location (alloc@sid:488@tid:Top Threads(#top)).hh.tbl (race with conf. 110): (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:514:7-514:37)
  write with lock:{lock} (conf. 110)  (exp: & e->hh.tbl) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:634:15-634:51)
  write with lock:{lock} (conf. 110)  (exp: & e->hh.tbl) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:657:13-657:37)
  read with [] (conf. 110)  (exp: & elts->hh.tbl) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:810:5-810:34)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:275:20-275:21)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 9U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:571:13-571:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:658:20-658:21)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 8U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:573:13-573:20)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 7U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:575:13-575:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:480:24-480:25)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 6U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:577:13-577:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:279:20-279:21)
[Warning][Deadcode][CWE-570] condition '_hj_k___0 == 5U' is always false (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:579:13-579:20)
[Warning][Deadcode][CWE-571] condition '_hj_k___0 == 4U' is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:581:13-581:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:666:18-666:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:281:24-281:25)
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 45
  vulnerable: 0
  unsafe: 3
  total memory locations: 48
