./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/goblint-regression/09-regions_22-nocollapse.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/goblint-regression/09-regions_22-nocollapse.i:1039:5-1043:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1035:3-1046:3 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:5-1057:71 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1054:3-1058:3 with factor 10
[Info] malloc wrapper: new
[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) )

[Info] runtime: 00:00:10.229
[Info] vars: 4152, evals: 3837

[Info] |called|=11

Memory statistics: total=25321.65MB, max=181.06MB, minor=25317.97MB, major=526.19MB, promoted=522.50MB
    minor collections=12084  major collections=24 compactions=0


[Info] runtime: 00:00:20.259
[Info] vars: 5586, evals: 6556

[Info] |called|=11

Memory statistics: total=53837.54MB, max=208.23MB, minor=53833.82MB, major=991.29MB, promoted=987.57MB
    minor collections=25687  major collections=33 compactions=0

[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1012:3-1012:27)
[Warning][Unknown] lval (& p)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1006:3-1006:20)
[Warning][Unknown] lval (& p)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1007:3-1007:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1007:3-1007:20)
[Warning][Unknown] lval (& p)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1008:1-1008:1)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Unknown] lval (& tmp___1)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1016:20-1016:38)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1017:3-1017:19)
[Warning][Unknown] lval (& tmp___1)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1017:3-1017:19)
[Warning][Unknown] Size of lval dereference expression next is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1017:3-1017:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer next is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1017:3-1017:19)
[Warning][Unknown] lval (& tmp___1)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1018:3-1018:19)
[Warning][Unknown] lval (& tmp___1)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1019:3-1019:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1019:3-1019:19)
[Warning][Unknown] lval (& tmp___1)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1020:3-1020:19)
[Warning][Unknown] lval (& tmp___1)->list points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1021:1-1021:1)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 400 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1006:3-1006:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 400 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1007:3-1007:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 400 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1016:20-1016:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 400 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1020:3-1020:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 480 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1006:3-1006:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 480 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1007:3-1007:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 480 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1016:20-1016:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 480 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1020:3-1020:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 560 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1006:3-1006:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 560 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1007:3-1007:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 560 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1016:20-1016:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 560 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1020:3-1020:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 640 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1006:3-1006:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 640 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1007:3-1007:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 640 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1016:20-1016:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 640 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1020:3-1020:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 720 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1006:3-1006:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 720 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1007:3-1007:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 720 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1016:20-1016:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 320 (in bytes). It is offset by 720 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1020:3-1020:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 11 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:34-1057:71)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1059:3-1059:17)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Program aborted while running in multi-threaded mode. A memory leak might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:11:14-11:21)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1036:5-1036:42)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1038:5-1038:70)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] unlocking mutex (c.slots_mutex[def_exc:Unknown int([0,31]); intervals:[0,9]; enums:not {} ([0,31])]) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1044:5-1044:44)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1036:5-1036:42)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1038:5-1038:70)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] unlocking mutex (c.slots_mutex[def_exc:Unknown int([-31,31]); intervals:[1,9]; enums:not {} ([-31,31])]) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1044:5-1044:44)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1036:5-1036:42)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1038:5-1038:70)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] unlocking mutex (c.slots_mutex[def_exc:Unknown int([-31,31]); intervals:[2,9]; enums:not {} ([-31,31])]) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1044:5-1044:44)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1036:5-1036:42)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1038:5-1038:70)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] unlocking mutex (c.slots_mutex[def_exc:Unknown int([-31,31]); intervals:[3,9]; enums:not {} ([-31,31])]) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1044:5-1044:44)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1036:5-1036:42)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1038:5-1038:70)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] unlocking mutex (c.slots_mutex[def_exc:Unknown int([-31,31]); intervals:[4,9]; enums:not {} ([-31,31])]) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1044:5-1044:44)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1036:5-1036:42)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1038:5-1038:70)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] unlocking mutex (c.slots_mutex[def_exc:Unknown int([-31,31]); intervals:[5,9]; enums:not {} ([-31,31])]) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1044:5-1044:44)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1036:5-1036:42)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1038:5-1038:70)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] unlocking mutex (c.slots_mutex[def_exc:Unknown int([-31,31]); intervals:[6,9]; enums:not {} ([-31,31])]) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1044:5-1044:44)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1036:5-1036:42)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1038:5-1038:70)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] unlocking mutex (c.slots_mutex[def_exc:Unknown int([-31,31]); intervals:[7,9]; enums:not {} ([-31,31])]) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1044:5-1044:44)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1036:5-1036:42)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1038:5-1038:70)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] unlocking mutex (c.slots_mutex[def_exc:Unknown int([-31,31]); intervals:[8,9]; enums:not {} ([-31,31])]) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1044:5-1044:44)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1038:5-1038:70)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1039:12-1039:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > BeforeStart] May access array before start (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1040:7-1040:19)
[Warning][Unknown] Pointer pos has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Unknown] Size of lval dereference expression pos is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > Other] Pointer pos contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer pos is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1041:7-1041:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1042:7-1042:72)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1063:10-1063:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1063:10-1063:18)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory may be leaked at thread return for thread [main] (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1063:10-1063:18)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:953@tid:[main](#4)), (alloc@sid:873@tid:[main](#0)), (alloc@sid:904@tid:[main](#0)), (alloc@sid:806@tid:[main](#4)), (alloc@sid:1002@tid:[main](#2)), (alloc@sid:757@tid:[main](#2)), (alloc@sid:642@tid:[main](#0)), (alloc@sid:677@tid:[main](#0)), (alloc@sid:1083@tid:[main](#0)), (alloc@sid:806@tid:[main](#3)), (alloc@sid:789@tid:[main](#0)), (alloc@sid:757@tid:[main](#0)), (alloc@sid:1051@tid:[main](#0)), (alloc@sid:1100@tid:[main](#0)), (alloc@sid:782@tid:[main](#0)), (alloc@sid:929@tid:[main](#0)), (alloc@sid:806@tid:[main](#1)), (alloc@sid:757@tid:[main]), (alloc@sid:684@tid:[main](#0)), (alloc@sid:855@tid:[main](#0)), (alloc@sid:1051@tid:[main](#4)), (alloc@sid:698@tid:[main](#0)), (alloc@sid:747@tid:[main](#0)), (alloc@sid:1100@tid:[main](#3)), (alloc@sid:708@tid:[main](#1)), (alloc@sid:757@tid:[main](#1)), (alloc@sid:978@tid:[main](#0)), (alloc@sid:845@tid:[main](#0)), (alloc@sid:953@tid:[main](#1)), (alloc@sid:708@tid:[main](#2)), (alloc@sid:943@tid:[main](#0)), (alloc@sid:904@tid:[main](#2)), (alloc@sid:971@tid:[main](#0)), (alloc@sid:880@tid:[main](#0)), (alloc@sid:953@tid:[main]), (alloc@sid:855@tid:[main](#3)), (alloc@sid:708@tid:[main](#0)), (alloc@sid:838@tid:[main](#0)), (alloc@sid:1027@tid:[main](#0)), (alloc@sid:855@tid:[main](#4)), (alloc@sid:726@tid:[main](#0)), (alloc@sid:831@tid:[main](#0)), (alloc@sid:1002@tid:[main]), (alloc@sid:757@tid:[main](#3)), (alloc@sid:1100@tid:[main](#2)), (alloc@sid:894@tid:[main](#0)), (alloc@sid:904@tid:[main]), (alloc@sid:708@tid:[main](#3)), (alloc@sid:953@tid:[main](#3)), (alloc@sid:659@tid:[main](#4)), (alloc@sid:1002@tid:[main](#0)), (alloc@sid:1076@tid:[main](#0)), (alloc@sid:904@tid:[main](#4)), (alloc@sid:1051@tid:[main](#1)), (alloc@sid:659@tid:[main](#1)), (alloc@sid:659@tid:[main](#0)), (alloc@sid:824@tid:[main](#0)), (alloc@sid:1069@tid:[main](#0)), (alloc@sid:904@tid:[main](#3)), (alloc@sid:1090@tid:[main](#0)), (alloc@sid:635@tid:[main](#0)), (alloc@sid:757@tid:[main](#4)), (alloc@sid:1002@tid:[main](#1)), (alloc@sid:740@tid:[main](#0)), (alloc@sid:806@tid:[main](#0)), (alloc@sid:1034@tid:[main](#0)), (alloc@sid:855@tid:[main](#2)), (alloc@sid:985@tid:[main](#0)), (alloc@sid:992@tid:[main](#0)), (alloc@sid:1002@tid:[main](#3)), (alloc@sid:691@tid:[main](#0)), (alloc@sid:796@tid:[main](#0)), (alloc@sid:1100@tid:[main]), (alloc@sid:1100@tid:[main](#4)), (alloc@sid:1051@tid:[main](#2)), (alloc@sid:1051@tid:[main](#3)), (alloc@sid:1100@tid:[main](#1)), (alloc@sid:953@tid:[main](#2)), (alloc@sid:936@tid:[main](#0)), (alloc@sid:708@tid:[main](#4)), (alloc@sid:659@tid:[main](#3)), (alloc@sid:659@tid:[main](#2)), (alloc@sid:775@tid:[main](#0)), (alloc@sid:806@tid:[main]), (alloc@sid:855@tid:[main]), (alloc@sid:1020@tid:[main](#0)), (alloc@sid:708@tid:[main]), (alloc@sid:628@tid:[main](#0)), (alloc@sid:806@tid:[main](#2)), (alloc@sid:649@tid:[main](#0)), (alloc@sid:1041@tid:[main](#0)), (alloc@sid:1002@tid:[main](#4)), (alloc@sid:733@tid:[main](#0)), (alloc@sid:953@tid:[main](#0)), (alloc@sid:922@tid:[main](#0)), (alloc@sid:904@tid:[main](#1)), (alloc@sid:659@tid:[main]), (alloc@sid:855@tid:[main](#1)), (alloc@sid:887@tid:[main](#0)), (alloc@sid:1051@tid:[main]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1063:10-1063:18)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1063:10-1063:18)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Possible memory leak: Memory was allocated in a multithreaded program, but not all threads are joined. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1063:10-1063:18)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:67:1-71:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:72:1-76:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:77:1-81:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:82:1-86:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:87:1-91:1)
[Warning][Deadcode] Function 'lookup' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1022:1-1028:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 46
  dead: 9 (9 in uncalled functions)
  total lines: 55
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1054:7-1054:30)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1054:7-1054:30)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1054:7-1054:30)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1054:7-1054:30)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1054:7-1054:30)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1054:7-1054:30)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1054:7-1054:30)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1054:7-1054:30)
[Warning][Deadcode][CWE-570] condition 'j < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1035:10-1035:16)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-570] condition 'i < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1054:7-1054:30)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1054:7-1054:30)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)

[Info] runtime: 00:00:30.331
[Info] vars: 5586, evals: 6900

[Info] |called|=0

Memory statistics: total=81907.78MB, max=316.69MB, minor=81903.69MB, major=1449.50MB, promoted=1445.42MB
    minor collections=39075  major collections=39 compactions=0

[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1054:7-1054:30)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
[Warning][Deadcode][CWE-571] condition 'j < 30' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i:1057:9-1057:32)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
[Info][Race] Memory locations race summary:
  safe: 205
  vulnerable: 0
  unsafe: 0
  total memory locations: 205
