./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/pthread-complex/bounded_buffer.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:9-1503:69 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:9-1506:73 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:9-1507:60 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:9-1539:9 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:9-1570:9 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1627:5-1637:5 with factor 3
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1647:5-1658:5 with factor 5
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1668:5-1673:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1674:5-1679:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1680:5-1681:52 with factor 25
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1682:5-1683:52 with factor 25
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: 43
functionCalls: 225
loops: 17
loopBreaks: 0
controlFlowStatements: 563
expressions: 3545
instructions: 616
integralVars: (5,69)
arrayVars: (3,2)
pointerVars: (3,30)

Complexity estimates:
File: 124202
Total: 124202
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )
[Info][Unsound] Unknown address in {&buffer} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1667:5-1667:33)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1667:5-1667:33)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1455:5-1455:59)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(pthread_cond_t, TComp(union __anonunion_pthread_cond_t_551659845, __data : TComp(struct __anonstruct___data_282018390, __lock : TInt(int, ), __futex : TInt(unsigned int, ), __total_seq : TInt(unsigned long long, ), __wakeup_seq : TInt(unsigned long long, ), __woken_seq : TInt(unsigned long long, ), __mutex : TPtr(TVoid(), ), __nwaiters : TInt(unsigned int, ), __broadcast_seq : TInt(unsigned int, ), , ), __size : TArray(TInt(char, ), Some(Const(Int(48,int,48))), ), __align : TInt(long long, ), , ), ),  __restrict  ), AddrOf(Mem(Lval(Var(bbuf, NoOffset)), Field(not_full:TNamed(pthread_cond_t, TComp(union __anonunion_pthread_cond_t_551659845, __data : TComp(struct __anonstruct___data_282018390, __lock : TInt(int, ), __futex : TInt(unsigned int, ), __total_seq : TInt(unsigned long long, ), __wakeup_seq : TInt(unsigned long long, ), __woken_seq : TInt(unsigned long long, ), __mutex : TPtr(TVoid(), ), __nwaiters : TInt(unsigned int, ), __broadcast_seq : TInt(unsigned int, ), , ), __size : TArray(TInt(char, ), Some(Const(Int(48,int,48))), ), __align : TInt(long long, ), , ), ), NoOffset)))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1457:5-1457:61)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1457:5-1457:61)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(pthread_cond_t, TComp(union __anonunion_pthread_cond_t_551659845, __data : TComp(struct __anonstruct___data_282018390, __lock : TInt(int, ), __futex : TInt(unsigned int, ), __total_seq : TInt(unsigned long long, ), __wakeup_seq : TInt(unsigned long long, ), __woken_seq : TInt(unsigned long long, ), __mutex : TPtr(TVoid(), ), __nwaiters : TInt(unsigned int, ), __broadcast_seq : TInt(unsigned int, ), , ), __size : TArray(TInt(char, ), Some(Const(Int(48,int,48))), ), __align : TInt(long long, ), , ), ),  __restrict  ), AddrOf(Mem(Lval(Var(bbuf, NoOffset)), Field(not_empty:TNamed(pthread_cond_t, TComp(union __anonunion_pthread_cond_t_551659845, __data : TComp(struct __anonstruct___data_282018390, __lock : TInt(int, ), __futex : TInt(unsigned int, ), __total_seq : TInt(unsigned long long, ), __wakeup_seq : TInt(unsigned long long, ), __woken_seq : TInt(unsigned long long, ), __mutex : TPtr(TVoid(), ), __nwaiters : TInt(unsigned int, ), __broadcast_seq : TInt(unsigned int, ), , ), __size : TArray(TInt(char, ), Some(Const(Int(48,int,48))), ), __align : TInt(long long, ), , ), ), NoOffset)))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1463:5-1463:62)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1463:5-1463:62)
[Info][Unsound] Unknown address in {&buffer} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95)
[Info][Unsound] Unknown value in {&(alloc@sid:37@tid:[main](#top))[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1631:9-1631:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1631:9-1631:67)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1527:9-1527:55)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1529:5-1529:46)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1532:11-1532:57)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1532:11-1532:57)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1532:11-1532:57)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1534:9-1534:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1534:9-1534:23)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1535:18-1535:64)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1537:13-1537:70)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1540:9-1540:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1540:9-1540:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1543:9-1543:36)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1544:9-1544:54)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1544:9-1544:54)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1545:13-1545:29)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1547:13-1547:60)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1551:5-1551:49)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1551:5-1551:49)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1551:5-1551:49)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1551:5-1551:49)
[Info][Imprecise] Invalidating expressions: Lval(Var(stdout, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Unknown address in stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1631:9-1631:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1631:9-1631:67)
[Info][Imprecise] Invalidating expressions: Lval(Var(stdout, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Unknown address in stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1631:9-1631:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1631:9-1631:67)
[Info][Imprecise] Invalidating expressions: Lval(Var(stdout, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Unknown address in stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1631:9-1631:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1631:9-1631:67)
[Info][Imprecise] Invalidating expressions: Lval(Var(stdout, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Unknown address in stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1636:9-1636:23)
[Info][Unsound] Unknown address in {&buffer} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95)
[Info][Unsound] Unknown value in {&(alloc@sid:37@tid:[main](#top))[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95)
[Info][Unsound] Unknown address in {&buffer} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95)
[Info][Unsound] Unknown value in {&(alloc@sid:37@tid:[main](#top))[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1649:9-1649:54)
[Info][Unsound] Unknown address in {&temp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1649:9-1649:54)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1649:9-1649:54)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1557:9-1557:78)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1559:5-1559:46)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1562:9-1562:33)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1564:9-1564:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1564:9-1564:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1565:16-1565:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1568:13-1568:71)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1571:9-1571:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1571:9-1571:23)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1574:5-1574:48)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1574:5-1574:48)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1574:5-1574:48)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1574:5-1574:48)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1575:5-1575:46)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1579:12-1579:36)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1583:9-1583:38)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1584:9-1584:53)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1584:9-1584:53)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1585:13-1585:29)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1587:13-1587:59)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1591:5-1591:49)
[Info][Unsound] Unknown mutex unlocked, base privatization unsound (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1591:5-1591:49)
[Warning][Unknown] unlocking unknown mutex which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1591:5-1591:49)
[Warning][Unknown] unlocking mutex (buffer.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1591:5-1591:49)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1654:13-1654:37)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1654:13-1654:37)
[Info][Imprecise] Invalidating expressions: Lval(Var(stdout, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Unknown address in stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1649:9-1649:54)
[Info][Unsound] Unknown address in {&temp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1649:9-1649:54)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1649:9-1649:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1654:13-1654:37)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1654:13-1654:37)
[Info][Imprecise] Invalidating expressions: Lval(Var(stdout, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Unknown address in stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1649:9-1649:54)
[Info][Unsound] Unknown address in {&temp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1649:9-1649:54)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1649:9-1649:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1654:13-1654:37)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1654:13-1654:37)
[Info][Imprecise] Invalidating expressions: Lval(Var(stdout, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Unknown address in stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1649:9-1649:54)
[Info][Unsound] Unknown address in {&temp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1649:9-1649:54)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1649:9-1649:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1654:13-1654:37)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1654:13-1654:37)
[Info][Imprecise] Invalidating expressions: Lval(Var(stdout, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Unknown address in stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1657:9-1657:23)
[Info][Unsound] Unknown address in {&buffer} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95)
[Info][Unsound] Unknown value in {&(alloc@sid:37@tid:[main](#top))[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95)
[Info][Unsound] Unknown address in {&buffer} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1684:5-1684:33)
[Info][Unsound] Unknown value in {&(alloc@sid:37@tid:[main](#top))[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1684:5-1684:33)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1684:5-1684:33)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1493:5-1493:46)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1496:5-1496:48)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1498:5-1498:49)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1499:5-1499:51)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(status2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1500:5-1500:52)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:51-1503:69)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1503:13-1503:49)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:55-1506:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1506:13-1506:53)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Analyzer] Pointer *(bbuf->buf + i) in function free doesn't evaluate to a valid address. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:42-1507:60)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1507:13-1507:40)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)bbuf->buf in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1509:5-1509:20)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1509:5-1509:20)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:351:1-355:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:356:1-360:1)
[Warning][Deadcode] Function 'bounded_buf_putcleanup' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1512:1-1517:1)
[Warning][Deadcode] Function 'bounded_buf_getcleanup' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1518:1-1523:1)
[Warning][Deadcode] Function 'bounded_buf_is_empty' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1594:1-1604:1)
[Warning][Deadcode] Function 'bounded_buf_is_full' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1605:1-1614:1)
[Warning][Deadcode] Function 'bounded_buf_destroy' has dead code:
  on line 1492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1492-1492)
[Warning][Deadcode] Function 'bounded_buf_init' has dead code:
  on lines 1477..1480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1477-1480)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 122
  dead: 30 (25 in uncalled functions)
  total lines: 152
[Warning][Deadcode][CWE-570] condition 'status != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1561:9-1561:20)
[Warning][Deadcode][CWE-571] condition 'status == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1577:9-1577:20)
[Warning][Deadcode][CWE-571] condition 'i < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1647:9-1647:27)
[Warning][Deadcode][CWE-570] condition 'status != 0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1592:5-1592:69)
[Warning][Race] Memory location (void *) (race with conf. 100):
  write with [mhp:{tid=[main, producer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95#top]}, thread:[main, producer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95#top]] (conf. 100)  (exp: & *(bbuf->buf + bbuf->rear)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1543:9-1543:36)
  write with [mhp:{tid=[main, producer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95#top]}, lock:{buffer.mutex}, thread:[main, producer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95#top]] (conf. 100)  (exp: & *(bbuf->buf + bbuf->rear)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1543:9-1543:36)
  write with [mhp:{tid=[main, producer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95#top]}, thread:[main, producer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95#top]] (conf. 100)  (exp: & *(bbuf->buf + bbuf->rear)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1543:9-1543:36)
  write with [mhp:{tid=[main, producer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95#top]}, lock:{buffer.mutex}, thread:[main, producer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1672:9-1672:95#top]] (conf. 100)  (exp: & *(bbuf->buf + bbuf->rear)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1543:9-1543:36)
  read with [mhp:{tid=[main, consumer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95#top]}, thread:[main, consumer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95#top]] (conf. 100)  (exp: & *(bbuf->buf + bbuf->head)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1583:9-1583:38)
  read with [mhp:{tid=[main, consumer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95#top]}, lock:{buffer.mutex}, thread:[main, consumer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95#top]] (conf. 100)  (exp: & *(bbuf->buf + bbuf->head)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1583:9-1583:38)
  read with [mhp:{tid=[main, consumer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95#top]}, thread:[main, consumer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95#top]] (conf. 100)  (exp: & *(bbuf->buf + bbuf->head)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1583:9-1583:38)
  read with [mhp:{tid=[main, consumer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95#top]}, lock:{buffer.mutex}, thread:[main, consumer_routine@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1678:9-1678:95#top]] (conf. 100)  (exp: & *(bbuf->buf + bbuf->head)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1583:9-1583:38)
[Warning][Deadcode][CWE-571] condition 'i < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1647:9-1647:27)
[Warning][Deadcode][CWE-571] condition 'i < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1647:9-1647:27)
[Warning][Deadcode][CWE-571] condition 'i < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1647:9-1647:27)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:12:73-12:74)
[Warning][Deadcode][CWE-570] condition 'i < 4' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1647:9-1647:27)
[Warning][Deadcode][CWE-570] condition '(unsigned long )bbuf == (unsigned long )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1453:9-1453:28)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1682:9-1682:27)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1682:9-1682:27)
[Warning][Deadcode][CWE-571] condition 'i < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1627:9-1627:27)
[Warning][Deadcode][CWE-570] condition 'i < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1682:9-1682:27)
[Warning][Deadcode][CWE-570] condition '(unsigned long )bbuf->buf == (unsigned long )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1475:9-1475:33)
[Warning][Deadcode][CWE-571] condition 'i < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1627:9-1627:27)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1668:9-1668:27)
[Warning][Deadcode][CWE-570] condition 'status != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1531:9-1531:20)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1674:9-1674:27)
[Warning][Deadcode][CWE-571] condition 'i < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1627:9-1627:27)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1668:9-1668:27)
[Warning][Deadcode][CWE-570] condition '(unsigned long )bbuf == (unsigned long )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1491:9-1491:55)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1680:9-1680:27)
[Warning][Deadcode][CWE-570] condition 'bbuf->valid != 0xACDEFA' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1491:9-1491:55)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1674:9-1674:27)
[Warning][Deadcode][CWE-570] condition 'status != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1494:9-1494:20)
[Warning][Deadcode][CWE-570] condition 'i < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1668:9-1668:27)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1680:9-1680:27)
[Warning][Deadcode][CWE-570] condition '(unsigned long )item == (unsigned long )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1557:9-1557:78)
[Warning][Deadcode][CWE-570] condition 'i < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1674:9-1674:27)
[Warning][Deadcode][CWE-570] condition 'i < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.i:1680:9-1680:27)
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 8
  vulnerable: 0
  unsafe: 1
  total memory locations: 9
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/pthread-complex/bounded_buffer.i:777 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.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/pthread-complex/bounded_buffer.i:774 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/bounded_buffer.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
