./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-data-race.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1806:7-1806:141 with factor 6
has Label
has Label
has Label
has Label
has Label
has Label
has Label
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:5-1808:16 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1811:7-1811:143 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1824:9-1824:146 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1828:9-1828:145 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1846:5-1846:150 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1849:5-1849:150 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1852:5-1852:148 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1855:5-1855:148 with factor 6
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
Collected factors:
functions: 37
functionCalls: 206
loops: 17
loopBreaks: 0
controlFlowStatements: 280
expressions: 1973
instructions: 379
integralVars: (10,52)
arrayVars: (3,0)
pointerVars: (5,23)

Complexity estimates:
File: 73983
Total: 73983
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(time_t, TNamed(__time_t, TInt(long, ), ), ), ), CastE(TPtr(TVoid(), ), Const(Int(0,int,0)))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1839:10-1839:43)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1839:10-1839:43)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1844:3-1844:89)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1804:5-1804:41)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1808:7-1808:16)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1809:5-1809:43)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1811:12-1811:120)
[Info][Unsound] Unknown address in {&tmp___0} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1811:12-1811:120)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1811:12-1811:120)
[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, _next : TPtr(TCompLoop(struct _IO_marker, _, ), ), _sbuf : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _pos : TInt(int, ), , ), ), _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, TNamed(__quad_t, TInt(long long, ), ), ), __pad1 : TPtr(TVoid(), ), __pad2 : TPtr(TVoid(), ), __pad3 : TPtr(TVoid(), ), __pad4 : TPtr(TVoid(), ), __pad5 : TNamed(size_t, TInt(unsigned int, ), ), _mode : TInt(int, ), _unused2 : TArray(TInt(char, ), Some(MinusA(MinusA(*(Const(Int(f,unsigned long,None)), sizeof(TInt(int, ))), *(Const(Int(4,unsigned long,None)), sizeof(TPtr(TVoid(), )))), sizeof(TNamed(size_t, TInt(unsigned int, ), )))), ), , ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1811:12-1811:120)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1811:12-1811:120)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1811:12-1811:120)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1811:12-1811:120)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(time_t, TNamed(__time_t, TInt(long, ), ), ), ), CastE(TPtr(TVoid(), ), Const(Int(0,int,0)))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1803:10-1803:39)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1803:10-1803:39)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1846:10-1846:127)
[Info][Unsound] Unknown address in {&tmp___0} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1846:10-1846:127)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1846:10-1846:127)
[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, _next : TPtr(TCompLoop(struct _IO_marker, _, ), ), _sbuf : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _pos : TInt(int, ), , ), ), _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, TNamed(__quad_t, TInt(long long, ), ), ), __pad1 : TPtr(TVoid(), ), __pad2 : TPtr(TVoid(), ), __pad3 : TPtr(TVoid(), ), __pad4 : TPtr(TVoid(), ), __pad5 : TNamed(size_t, TInt(unsigned int, ), ), _mode : TInt(int, ), _unused2 : TArray(TInt(char, ), Some(MinusA(MinusA(*(Const(Int(f,unsigned long,None)), sizeof(TInt(int, ))), *(Const(Int(4,unsigned long,None)), sizeof(TPtr(TVoid(), )))), sizeof(TNamed(size_t, TInt(unsigned int, ), )))), ), , ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1846:10-1846:127)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1846:10-1846:127)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1846:10-1846:127)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1846:10-1846:127)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1847:3-1847:89)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1821:5-1821:44)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1830:7-1830:15)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1824:14-1824:123)
[Info][Unsound] Unknown address in {&tmp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1824:14-1824:123)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1824:14-1824:123)
[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, _next : TPtr(TCompLoop(struct _IO_marker, _, ), ), _sbuf : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _pos : TInt(int, ), , ), ), _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, TNamed(__quad_t, TInt(long long, ), ), ), __pad1 : TPtr(TVoid(), ), __pad2 : TPtr(TVoid(), ), __pad3 : TPtr(TVoid(), ), __pad4 : TPtr(TVoid(), ), __pad5 : TNamed(size_t, TInt(unsigned int, ), ), _mode : TInt(int, ), _unused2 : TArray(TInt(char, ), Some(MinusA(MinusA(*(Const(Int(f,unsigned long,None)), sizeof(TInt(int, ))), *(Const(Int(4,unsigned long,None)), sizeof(TPtr(TVoid(), )))), sizeof(TNamed(size_t, TInt(unsigned int, ), )))), ), , ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1824:14-1824:123)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1824:14-1824:123)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1824:14-1824:123)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1824:14-1824:123)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1826:7-1826:45)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1828:14-1828:122)
[Info][Unsound] Unknown address in {&tmp___0} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1828:14-1828:122)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1828:14-1828:122)
[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, _next : TPtr(TCompLoop(struct _IO_marker, _, ), ), _sbuf : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _pos : TInt(int, ), , ), ), _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, TNamed(__quad_t, TInt(long long, ), ), ), __pad1 : TPtr(TVoid(), ), __pad2 : TPtr(TVoid(), ), __pad3 : TPtr(TVoid(), ), __pad4 : TPtr(TVoid(), ), __pad5 : TNamed(size_t, TInt(unsigned int, ), ), _mode : TInt(int, ), _unused2 : TArray(TInt(char, ), Some(MinusA(MinusA(*(Const(Int(f,unsigned long,None)), sizeof(TInt(int, ))), *(Const(Int(4,unsigned long,None)), sizeof(TPtr(TVoid(), )))), sizeof(TNamed(size_t, TInt(unsigned int, ), )))), ), , ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1828:14-1828:122)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1828:14-1828:122)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1828:14-1828:122)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1828:14-1828:122)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(time_t, TNamed(__time_t, TInt(long, ), ), ), ), CastE(TPtr(TVoid(), ), Const(Int(0,int,0)))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1819:10-1819:39)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1819:10-1819:39)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1849:10-1849:127)
[Info][Unsound] Unknown address in {&tmp___1} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1849:10-1849:127)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1849:10-1849:127)
[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, _next : TPtr(TCompLoop(struct _IO_marker, _, ), ), _sbuf : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _pos : TInt(int, ), , ), ), _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, TNamed(__quad_t, TInt(long long, ), ), ), __pad1 : TPtr(TVoid(), ), __pad2 : TPtr(TVoid(), ), __pad3 : TPtr(TVoid(), ), __pad4 : TPtr(TVoid(), ), __pad5 : TNamed(size_t, TInt(unsigned int, ), ), _mode : TInt(int, ), _unused2 : TArray(TInt(char, ), Some(MinusA(MinusA(*(Const(Int(f,unsigned long,None)), sizeof(TInt(int, ))), *(Const(Int(4,unsigned long,None)), sizeof(TPtr(TVoid(), )))), sizeof(TNamed(size_t, TInt(unsigned int, ), )))), ), , ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1849:10-1849:127)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1849:10-1849:127)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1849:10-1849:127)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1849:10-1849:127)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1850:3-1850:57)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1852:10-1852:125)
[Info][Unsound] Unknown address in {&tmp___2} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1852:10-1852:125)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1852:10-1852:125)
[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, _next : TPtr(TCompLoop(struct _IO_marker, _, ), ), _sbuf : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _pos : TInt(int, ), , ), ), _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, TNamed(__quad_t, TInt(long long, ), ), ), __pad1 : TPtr(TVoid(), ), __pad2 : TPtr(TVoid(), ), __pad3 : TPtr(TVoid(), ), __pad4 : TPtr(TVoid(), ), __pad5 : TNamed(size_t, TInt(unsigned int, ), ), _mode : TInt(int, ), _unused2 : TArray(TInt(char, ), Some(MinusA(MinusA(*(Const(Int(f,unsigned long,None)), sizeof(TInt(int, ))), *(Const(Int(4,unsigned long,None)), sizeof(TPtr(TVoid(), )))), sizeof(TNamed(size_t, TInt(unsigned int, ), )))), ), , ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1852:10-1852:125)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1852:10-1852:125)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1852:10-1852:125)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1852:10-1852:125)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1853:3-1853:57)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___3, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1855:10-1855:125)
[Info][Unsound] Unknown address in {&tmp___3} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1855:10-1855:125)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1855:10-1855:125)
[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, _next : TPtr(TCompLoop(struct _IO_marker, _, ), ), _sbuf : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _pos : TInt(int, ), , ), ), _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, TNamed(__quad_t, TInt(long long, ), ), ), __pad1 : TPtr(TVoid(), ), __pad2 : TPtr(TVoid(), ), __pad3 : TPtr(TVoid(), ), __pad4 : TPtr(TVoid(), ), __pad5 : TNamed(size_t, TInt(unsigned int, ), ), _mode : TInt(int, ), _unused2 : TArray(TInt(char, ), Some(MinusA(MinusA(*(Const(Int(f,unsigned long,None)), sizeof(TInt(int, ))), *(Const(Int(4,unsigned long,None)), sizeof(TPtr(TVoid(), )))), sizeof(TNamed(size_t, TInt(unsigned int, ), )))), ), , ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1855:10-1855:125)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1855:10-1855:125)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1855:10-1855:125)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1855:10-1855:125)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:62:1-66:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:67:1-71:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:72:1-76:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:77:1-81:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:82:1-86:1)
[Warning][Deadcode] Function 'counter_thread' has dead code:
  on line 1806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1806-1806)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 44
  dead: 6 (5 in uncalled functions)
  total lines: 50
[Warning][Deadcode][CWE-571] condition 'spin < 10000000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:9-1807:43)
[Warning][Race] Memory location strerror (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1290:13-1290:38)
  call with [region:{strerror}, mhp:{tid=[main, counter_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1844:3-1844:89#top]}, thread:[main, counter_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1844:3-1844:89#top]] (conf. 110)  (exp: strerror) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1811:12-1811:120)
  call with [region:{strerror}, mhp:{tid=[main, monitor_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1847:3-1847:89#top]}, thread:[main, monitor_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1847:3-1847:89#top]] (conf. 110)  (exp: strerror) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1824:14-1824:123)
  call with [region:{strerror}, mhp:{tid=[main, monitor_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1847:3-1847:89#top]}, thread:[main, monitor_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1847:3-1847:89#top]] (conf. 110)  (exp: strerror) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1828:14-1828:122)
  call with [region:{strerror}, mhp:{tid=[main]; created={[main, counter_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1844:3-1844:89#top]}}, thread:[main]] (conf. 110)  (exp: strerror) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1846:10-1846:127)
  call with [region:{strerror}, mhp:{tid=[main]; created={[main, counter_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1844:3-1844:89#top], [main, monitor_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1847:3-1847:89#top]}}, thread:[main]] (conf. 110)  (exp: strerror) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1849:10-1849:127)
  call with [region:{strerror}, mhp:{tid=[main]; created={[main, counter_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1844:3-1844:89#top], [main, monitor_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1847:3-1847:89#top]}; must_joined={[main, counter_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1844:3-1844:89#top]}}, thread:[main]] (conf. 110)  (exp: strerror) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1852:10-1852:125)
[Warning][Deadcode][CWE-571] condition 'spin < 10000000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:9-1807:43)
[Warning][Deadcode][CWE-571] condition 'spin < 10000000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:9-1807:43)
[Warning][Deadcode][CWE-571] condition 'spin < 10000000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:9-1807:43)
[Warning][Deadcode][CWE-571] condition 'spin < 10000000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:9-1807:43)
[Warning][Deadcode][CWE-571] condition 'spin < 10000000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:9-1807:43)
[Warning][Deadcode][CWE-571] condition 'spin < 10000000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:9-1807:43)
[Warning][Deadcode][CWE-570] condition 'status != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1805:9-1805:20)
[Warning][Deadcode][CWE-571] condition 'spin < 10000000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:9-1807:43)
[Warning][Deadcode][CWE-571] condition 'spin < 10000000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:9-1807:43)
[Warning][Deadcode][CWE-571] condition 'spin < 10000000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:9-1807:43)
[Warning][Deadcode][CWE-571] condition 'spin < 10000000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:9-1807:43)
[Warning][Deadcode][CWE-571] condition 'spin < 10000000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1807:9-1807:43)
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 3
  vulnerable: 0
  unsafe: 1
  total memory locations: 4
lib/libc/stub/src/stdlib.c:6: Warning: Incompatible declaration for qsort (from .goblint/preprocessed/stdlib.i(3)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1168 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i (0)) 
	Failed assumption that size_t and size_t are isomorphic (different integer types unsigned int  and unsigned long ) 
lib/libc/stub/src/stdlib.c:37: Warning: Incompatible declaration for bsearch (from .goblint/preprocessed/stdlib.i(3)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i:1165 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_36-trylock_nr.i (0)) 
	Failed assumption that size_t and size_t are isomorphic (different integer types unsigned int  and unsigned long ) 
lib/libc/stub/src/stdlib.c:7: Warning: The name qsort is used for two distinct globals
lib/libc/stub/src/stdlib.c:38: Warning: The name bsearch is used for two distinct globals
