./goblint --conf conf/svcomp23.json --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.
unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
unrolling loop at /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:275:13-278:13 with factor 25
unrolling loop at /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:281:17-284:17 with factor 25
unrolling loop at /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:298:19-301:19 with factor 25
unrolling loop at /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:474:13-477:13 with factor 25
unrolling loop at /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:480:17-483:17 with factor 25
unrolling loop at /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:497:19-500:19 with factor 25
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
unrolling loop at /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:632:13-654:13 with factor 3
unrolling loop at /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:658:13-664:13 with factor 6
unrolling loop at /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:668:13-671:13 with factor 25
unrolling loop at /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:702:27-705:27 with factor 25
Collected factors:
functions: 33
functionCalls: 94
loops: 48
loopBreaks: 0
controlFlowStatements: 1014
expressions: 5190
instructions: 741
integralVars: (4,69)
arrayVars: (2,0)
pointerVars: (2,31)

Complexity estimates:
File: 634310
thread created by pthread_create, called by:
  main
Total: 634310
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )
[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][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:777:3-778:79)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:160:5-160:40)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:162:7-162:98)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:162:7-162:98)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:162:7-162:98)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:162:7-162:98)
[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(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:160:5-160:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:789:3-790:79)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:359:5-359:40)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:361:7-361:99)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:361:7-361:99)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:361:7-361:99)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:361:7-361:99)
[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(status,
                                     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:803:3-803: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(status, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:807:3-807:52)
[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, TCompLoop(struct _IO_FILE, _, ), ),  __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)
[Warning][Deadcode] Function 'thread_routine_r' has dead code:
  on lines 165..206 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:165-206)
  on lines 209..210 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:209-210)
  on line 212 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:212-212)
  on lines 214..235 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:214-235)
  on lines 238..265 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:238-265)
  on lines 272..276 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:272-276)
  on lines 279..282 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:279-282)
  on line 286 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:286-286)
  on lines 288..292 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:288-292)
  on lines 297..299 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:297-299)
  on line 303 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:303-303)
  on lines 314..315 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:314-315)
  on lines 317..318 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:317-318)
  on line 320 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:320-320)
[Warning][Deadcode] Function 'thread_routine_w' has dead code:
  on lines 364..405 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:364-405)
  on lines 408..409 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:408-409)
  on line 411 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:411-411)
  on lines 413..434 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:413-434)
  on lines 437..464 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:437-464)
  on lines 471..475 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:471-475)
  on lines 478..481 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:478-481)
  on line 485 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:485-485)
  on lines 487..491 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:487-491)
  on lines 496..498 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:496-498)
  on line 502 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:502-502)
  on lines 513..517 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:513-517)
  on lines 519..559 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:519-559)
  on lines 562..563 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:562-563)
  on line 565 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:565-565)
  on lines 567..588 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:567-588)
  on lines 591..618 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:591-618)
  on lines 625..636 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:625-636)
  on lines 638..648 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:638-648)
  on line 650 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:650-650)
  on line 655 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:655-655)
  on lines 657..662 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:657-662)
  on lines 666..669 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:666-669)
  on lines 672..678 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:672-678)
  on lines 680..687 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:680-687)
  on lines 689..691 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:689-691)
  on line 693 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:693-693)
  on lines 695..703 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:695-703)
  on lines 706..711 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:706-711)
  on lines 714..717 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:714-717)
  on lines 719..720 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:719-720)
  on line 722 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:722-722)
  on lines 724..729 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:724-729)
  on line 731 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:731-731)
  on lines 733..735 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:733-735)
  on lines 751..752 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:751-752)
  on line 754 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:754-754)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 55
  dead: 421
  total: 476
[Warning][Deadcode][CWE-571] condition 'i < 100000' is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:358:10-358:20)
[Warning][Deadcode][CWE-571] condition 'tmp != 0' is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:360:9-360:17)
[Warning][Deadcode][CWE-571] condition 'i < 100000' is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:159:10-159:20)
[Warning][Deadcode][CWE-571] condition 'tmp != 0' is always true (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:161:9-161:17)
SV-COMP result: true
[Info][Race] Memory locations race summary:
  safe: 1
  vulnerable: 0
  unsafe: 0
  total: 1
