./goblint --conf conf/svcomp25.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-free) ) -> enabling soundness analyses "base, useAfterFree"[0;0;00m
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-deref) ) -> enabling soundness analyses "base, memOutOfBounds"[0;0;00m
[0;34m[Info] Setting "ana.arrayoob" to true[0;0;00m
[0;34m[Info] Setting "cil.addNestedScopeAttr" to true[0;0;00m
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-memtrack) ) -> enabling soundness analyses "memLeak"[0;0;00m
[0;34m[Info] Setting "ana.malloc.unique_address_count" to 5[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1011:5-1016:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1029:5-1035:5 with factor 4
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain ONLY for:
[Info] stored_elements, abort, i, count, tmp, key, a, count, i, j, i___0, j___0, k, size, r, top, expression, tmp___0, id1, id2, tmp, i, tmp___0, tmp___1, tmp, i, value, q, x, q, x, q, __x, __x, __x
[Info] SV-COMP specification: CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1047:3-1047:15)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12800 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:954:3-954:12)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12832 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:955:3-955:12)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12864 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:956:3-956:14)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1048:7-1048:27)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12800 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:960:7-960:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12832 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:960:7-960:25)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1052:3-1052:48)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1014:7-1014:28)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:980:3-980:26)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression (1611) (in bytes) with offset by ((Unknown int([-31,31]),[0,12800],not {} ([-31,31]),32ℤ)) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:980:3-980:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:981:3-981:14)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12864 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:981:3-981:14)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12832 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:982:7-982:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12832 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:984:5-984:16)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12832 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:988:5-988:14)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1014:7-1014:28)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression (1611) (in bytes) with offset by ((Unknown int([-31,31]),[32,12800],not {} ([-31,31]),32ℤ)) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:980:3-980:26)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1014:7-1014:28)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1014:7-1014:28)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1014:7-1014:28)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1053:3-1053:48)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1031:11-1031:30)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1032:13-1032:49)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:995:3-995:26)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression (1611) (in bytes) with offset by ((Unknown int([-31,31]),[0,12800],not {} ([-31,31]),32ℤ)) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:995:3-995:26)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:996:3-996:14)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12864 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:996:3-996:14)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12800 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:997:7-997:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12800 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:999:5-999:16)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 1611 (in bytes). It is offset by 12800 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1002:5-1002:14)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1031:11-1031:30)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1032:13-1032:49)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1031:11-1031:30)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1032:13-1032:49)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1031:11-1031:30)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1032:13-1032:49)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1031:11-1031:30)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1032:13-1032:49)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:76:1-80:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:81:1-85:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:86:1-90:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:91:1-95:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:96:1-100:1)
[Warning][Deadcode] Function 'full' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:968:1-977:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 1049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1049-1049)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 59
  dead: 10 (9 in uncalled functions)
  total lines: 69
[Warning][Deadcode][CWE-571] condition 'i < 400' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1011:8-1011:26)
[Warning][Deadcode][CWE-571] condition 'tmp' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1048:7-1048:27)
[Warning][Deadcode][CWE-570] condition 'tmp___0 == -1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1048:7-1048:27)
[Warning][Deadcode][CWE-571] condition 'i < 400' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1029:8-1029:26)
[Warning][Deadcode][CWE-571] condition 'i < 400' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1029:8-1029:26)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:21:73-21:74)
[Warning][Deadcode][CWE-571] condition 'i < 400' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1029:8-1029:26)
[Warning][Deadcode][CWE-571] condition 'i < 400' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1029:8-1029:26)
[Warning][Deadcode][CWE-571] condition 'i < 400' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1011:8-1011:26)
[Warning][Deadcode][CWE-571] condition 'i < 400' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1011:8-1011:26)
[Warning][Deadcode][CWE-571] condition 'i < 400' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longer.i:1011:8-1011:26)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
[Info][Race] Memory locations race summary:
  safe: 7
  vulnerable: 0
  unsafe: 0
  total memory locations: 7
