./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_valid-memsafety/basename-1.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_valid-memsafety/basename-1.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.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/busybox-1.22.0/basename-1.i:1447:5-1453:5 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1466:3-1477:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1501:3-1509:35 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1518:3-1519:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1520:3-1521:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1572:3-1573:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1579:3-1585:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1599:3-1600:34 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:5-1615:42 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1609:3-1616:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1618:3-1619:23 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[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][Witness] couldn't parse entry: find uuid
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:9:14-9:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1606:8-1606:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1606:8-1606:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1606:8-1606:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1607:8-1607:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1607:8-1607:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1607:8-1607:50)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1608:3-1608:15)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1608:3-1608:15)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1608:3-1608:15)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[-17179869184,17179869176],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1608:3-1608:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Unknown] Pointer *(argv + i___0) + 10 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + 10 is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + 10 is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[48,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[48,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1611:5-1611:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[48,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1612:5-1612:25)
[Warning][Unknown] Pointer *(argv + i___0) + 10 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + 10 is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + 10 is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[48,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1613:5-1613:20)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[48,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[48,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[48,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[48,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[48,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[48,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[48,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) + j has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Size of lval dereference expression *(argv + i___0) + j is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > Other] Pointer *(argv + i___0) contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Unknown] Pointer *(argv + i___0) has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer *(argv + i___0) in expression *(argv + i___0) + j is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[48,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1615:7-1615:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1334:6-1334:46)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1334:6-1334:46)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1334:6-1334:46)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1334:6-1334:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1354:7-1354:52)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1354:7-1354:52)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1354:7-1354:52)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1354:7-1354:52)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1356:7-1356:109)
[Warning][Unknown] Pointer __s2 + 0L has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1356:7-1356:109)
[Warning][Unknown] Size of lval dereference expression __s2 + 0L is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1356:7-1356:109)
[Warning][Behavior > Undefined > Other] Pointer __s2 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1356:7-1356:109)
[Warning][Unknown] Pointer __s2 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1356:7-1356:109)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer __s2 in expression __s2 + 0L is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1356:7-1356:109)
[Warning][Unknown] Pointer __s2 + 1L has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1361:11-1361:113)
[Warning][Unknown] Size of lval dereference expression __s2 + 1L is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1361:11-1361:113)
[Warning][Behavior > Undefined > Other] Pointer __s2 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1361:11-1361:113)
[Warning][Unknown] Pointer __s2 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1361:11-1361:113)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1361:11-1361:113)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer __s2 in expression __s2 + 1L is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1361:11-1361:113)
[Warning][Unknown] Pointer __s2 + 2L has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1366:15-1366:117)
[Warning][Unknown] Size of lval dereference expression __s2 + 2L is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1366:15-1366:117)
[Warning][Behavior > Undefined > Other] Pointer __s2 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1366:15-1366:117)
[Warning][Unknown] Pointer __s2 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1366:15-1366:117)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1366:15-1366:117)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer __s2 in expression __s2 + 2L is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1366:15-1366:117)
[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:857(#0)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:22:83-22:162)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:22:83-22:162)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1383:7-1383:77)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1383:7-1383:77)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1383:7-1383:77)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1383:7-1383:77)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (⊤) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1383:7-1383:77)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1390:7-1390:22)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1393:6-1393:44)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1393:6-1393:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1396:3-1396:44)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1396:3-1396:44)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1396:3-1396:44)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1396:3-1396:44)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (⊤) (in bytes) with offset by ((Unknown int([0,16]),[8,16],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1396:3-1396:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1444:3-1444:31)
[Warning][Unknown] Pointer s has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1484:8-1484:30)
[Warning][Unknown] Size of lval dereference expression s is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1484:8-1484:30)
[Warning][Behavior > Undefined > Other] Pointer s contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1484:8-1484:30)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer s is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1484:8-1484:30)
[Warning][Behavior > Undefined > Other] Pointer s contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1488:7-1488:38)
[Warning][Unknown] Pointer s has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1488:7-1488:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer s is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1488:7-1488:38)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1489:7-1489:56)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1490:7-1490:34)
[Warning][Unknown] Pointer s has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1491:10-1491:29)
[Warning][Unknown] Size of lval dereference expression s is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1491:10-1491:29)
[Warning][Behavior > Undefined > Other] Pointer s contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1491:10-1491:29)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer s is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1491:10-1491:29)
[Warning][Unknown] Pointer slash has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression slash is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer slash contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer slash is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer tmp_post$1 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression tmp_post$1 is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer tmp_post$1 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer tmp_post$1 is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer slash has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression slash is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer slash contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer slash is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer tmp_post$1 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression tmp_post$1 is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer tmp_post$1 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer tmp_post$1 is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer slash has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression slash is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer slash contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer slash is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer tmp_post$1 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression tmp_post$1 is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer tmp_post$1 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer tmp_post$1 is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer slash has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression slash is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer slash contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer slash is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer tmp_post$1 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression tmp_post$1 is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer tmp_post$1 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer tmp_post$1 is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer slash has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression slash is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer slash contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer slash is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer tmp_post$1 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression tmp_post$1 is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer tmp_post$1 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer tmp_post$1 is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer slash has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression slash is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer slash contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer slash is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer tmp_post$1 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression tmp_post$1 is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer tmp_post$1 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer tmp_post$1 is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer slash has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression slash is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer slash contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer slash is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer tmp_post$1 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression tmp_post$1 is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer tmp_post$1 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer tmp_post$1 is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer slash has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression slash is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer slash contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer slash is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer tmp_post$1 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression tmp_post$1 is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer tmp_post$1 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer tmp_post$1 is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer slash has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression slash is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer slash contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer slash is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Pointer tmp_post$1 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Unknown] Size of lval dereference expression tmp_post$1 is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > Other] Pointer tmp_post$1 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer tmp_post$1 is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1447:8-1447:59)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1455:3-1455:93)
[Info][Imprecise] Invalidating expressions: & slash (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1424:3-1424:26)
[Warning][Behavior > Undefined > Other] Pointer path contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1424:3-1424:26)
[Warning][Unknown] Pointer path has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1424:3-1424:26)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer path is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1424:3-1424:26)
[Warning][Unknown] Pointer slash + 1L has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1432:7-1432:121)
[Warning][Unknown] Size of lval dereference expression slash + 1L is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1432:7-1432:121)
[Warning][Behavior > Undefined > Other] Pointer slash contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1432:7-1432:121)
[Warning][Unknown] Pointer slash has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1432:7-1432:121)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1432:7-1432:121)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer slash in expression slash + 1L is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1432:7-1432:121)
[Warning][Behavior > Undefined > Other] Pointer s contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1397:3-1397:14)
[Warning][Unknown] Pointer s has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1397:3-1397:14)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer s is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1397:3-1397:14)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1400:6-1400:39)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1400:6-1400:39)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1400:6-1400:39)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (⊤) (in bytes) with offset by ((Unknown int([0,16]),[16,24],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1400:6-1400:39)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1402:5-1402:20)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1402:5-1402:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1402:5-1402:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (⊤) (in bytes) with offset by ((Unknown int([0,16]),[16,24],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1402:5-1402:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1408:7-1408:99)
[Warning][Behavior > Undefined > Other] Pointer s contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1408:7-1408:99)
[Warning][Unknown] Pointer s has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1408:7-1408:99)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer s is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1408:7-1408:99)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1408:7-1408:99)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1408:7-1408:99)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (⊤) (in bytes) with offset by ((Unknown int([0,16]),[16,24],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1408:7-1408:99)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1411:9-1411:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1415:3-1415:14)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1416:3-1416:44)
[Warning][Unknown] Pointer s + (long )tmp_post$8 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1416:3-1416:44)
[Warning][Unknown] Size of lval dereference expression s + (long )tmp_post$8 is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1416:3-1416:44)
[Warning][Behavior > Undefined > Other] Pointer s contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1416:3-1416:44)
[Warning][Unknown] Pointer s has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1416:3-1416:44)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1416:3-1416:44)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer s in expression s + (long )tmp_post$8 is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1416:3-1416:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1418:3-1418:62)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1468:5-1468:32)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1503:5-1503:28)
[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:857(#0)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:9:14-9:21)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Warning][Unknown] Size of lval dereference expression bb_errno is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer bb_errno is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1503:5-1503:28)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Warning][Unknown] Size of lval dereference expression bb_errno is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer bb_errno is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1503:5-1503:28)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Warning][Unknown] Size of lval dereference expression bb_errno is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer bb_errno is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1503:5-1503:28)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Warning][Unknown] Size of lval dereference expression bb_errno is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer bb_errno is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1503:5-1503:28)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Warning][Unknown] Size of lval dereference expression bb_errno is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer bb_errno is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1505:7-1505:90)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1466:6-1466:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1468:5-1468:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1475:5-1475:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1466:6-1466:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1468:5-1468:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1475:5-1475:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1466:6-1466:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1468:5-1468:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1475:5-1475:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1466:6-1466:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1468:5-1468:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1475:5-1475:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1466:6-1466:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1475:5-1475:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1466:6-1466:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1468:5-1468:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1419:10-1419:71)
[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:857(#0)), (alloc@sid:867(#0)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:22:83-22:162)
[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:857(#0)), (alloc@sid:867(#0)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:9:14-9:21)
[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:940(#0)), (alloc@sid:857(#0)), (alloc@sid:867(#0)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:22:83-22:162)
[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:940(#0)), (alloc@sid:857(#0)), (alloc@sid:867(#0)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:9:14-9:21)
[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:940(#0)), (alloc@sid:857(#0)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:22:83-22:162)
[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:940(#0)), (alloc@sid:857(#0)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:9:14-9:21)
[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:940(#0)), (alloc@sid:857(#0)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:940(#2)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:22:83-22:162)
[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:940(#0)), (alloc@sid:857(#0)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:940(#2)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:9:14-9:21)
[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:940(#0)), (alloc@sid:857(#0)), (alloc@sid:940(#3)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:940(#2)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:22:83-22:162)
[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:940(#0)), (alloc@sid:857(#0)), (alloc@sid:940(#3)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:940(#2)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:9:14-9:21)
[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:940(#0)), (alloc@sid:857(#0)), (alloc@sid:940(#3)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:940(#2)), (alloc@sid:940(#4)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:22:83-22:162)
[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:940(#0)), (alloc@sid:857(#0)), (alloc@sid:940(#3)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:940(#2)), (alloc@sid:940(#4)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:9:14-9:21)
[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:940(#0)), (alloc@sid:857(#0)), (alloc@sid:940), (alloc@sid:940(#3)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:940(#2)), (alloc@sid:940(#4)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:22:83-22:162)
[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:940(#0)), (alloc@sid:857(#0)), (alloc@sid:940), (alloc@sid:940(#3)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:940(#2)), (alloc@sid:940(#4)), (alloc@sid:859(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:9:14-9:21)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (0). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (8). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (16). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (24). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (32). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (40). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (48). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (56). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (64). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (72). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (80). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset (88). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of lval dereference expression ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]))) (in bytes) with offset by (0) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (⊤) with offset ((Unknown int([-63,63]),[96,17179869168],not {} ([-63,63]))). Memory out-of-bounds access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1619:5-1619:23)
[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:940(#0)), (alloc@sid:940), (alloc@sid:940(#3)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:940(#2)), (alloc@sid:940(#4)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1623:10-1623:13)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1623:10-1623:13)
[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:940(#0)), (alloc@sid:940(#3)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:940(#2)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1623:10-1623:13)
[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:940(#0)), (alloc@sid:940(#3)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:940(#2)), (alloc@sid:940(#4)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1623:10-1623:13)
[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:940(#0)), (alloc@sid:940(#1)), (alloc@sid:867(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1623:10-1623:13)
[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:940(#0)), (alloc@sid:940(#1)), (alloc@sid:867(#0)), (alloc@sid:940(#2)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1623:10-1623:13)
[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:940(#0)), (alloc@sid:867(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1623:10-1623:13)
[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:867(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1623:10-1623:13)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:76:1-80:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:81:1-85:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1321:1-1323:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1513:1-1523:1)
[Warning][Deadcode] Function 'getopt' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1524:1-1550:1)
[Warning][Deadcode] Function 'getopt_long' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1551:1-1557:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1558:1-1566:1)
[Warning][Deadcode] Function 'vasprintf' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1567:1-1588:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 131
  dead: 51 (51 in uncalled functions)
  total lines: 182
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-570] condition '! (total == 0l)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1471:10-1471:24)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:22:73-22:74)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1338:8-1338:16)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1599:6-1599:25)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition '__s2_len < 4UL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1343:7-1343:107)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1599:6-1599:25)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1599:6-1599:25)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1599:6-1599:25)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1599:6-1599:25)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1599:6-1599:25)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1599:6-1599:25)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1599:6-1599:25)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/basename-1.i:1614:8-1614:27)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
