./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.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
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2401:3-2412:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2434:3-2435:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2461:7-2467:22 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2479:5-2485:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2492:5-2509:20 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2516:9-2519:9 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2601:13-2604:13 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2689:25-2695:23 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2717:5-2736:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2746:5-2749:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2775:3-2784:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:3-2819:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2829:3-2837:35 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2844:3-2852:35 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:5-2928:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2939:3-2947:52 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3016:11-3030:11 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3069:3-3070:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3071:3-3072:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3123:3-3124:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3130:3-3136:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3150:3-3151:34 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3165:5-3166:42 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3160:3-3167:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3169:3-3170: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] longjmp -> enabling longjmp analyses "activeLongjmp, activeSetjmp, taintPartialContexts, modifiedSinceSetjmp, poisonVariables, expsplit, vla"
[Info] Setting "ana.int.interval" to true
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3157:8-3157:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3157:8-3157:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3157:8-3157:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3158:8-3158:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3158:8-3158:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3158:8-3158:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3166:7-3166:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3166:7-3166:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2434:6-2434:82)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2456:5-2456:47)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2460:7-2460:68)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2756:7-2756:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2756:7-2756:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2770:13-2770:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2765:11-2765:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2954:3-2954:92)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2960:3-2960:114)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2990:6-2990:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2993:5-2993:99)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3000:19-3000:73)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3000:19-3000:73)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3009:5-3009:35)
[Info][Unsound] Unknown address in {&e} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3009:5-3009:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3009:5-3009:35)
[Info][Imprecise] Invalidating expressions: (char ** __restrict  )end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2277:3-2277:25)
[Info][Imprecise] Invalidating expressions: & v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2277:3-2277:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3031:12-3031:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3042:11-3042:141)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2229:3-2229:49)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2297:3-2297:29)
[Info][Unsound] Unknown address in {&msg} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2297:3-2297:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2297:3-2297:29)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2302:3-2302:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2302:3-2302:74)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)msg in function realloc is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2317:3-2317:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2317:3-2317:116)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2317:3-2317:116)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2317:3-2317:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2333:5-2333:29)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2335:5-2335:54)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2336:5-2336:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2352:5-2352:29)
[Info][Imprecise] Invalidating expressions: (struct _IO_FILE *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2373:3-2373:63)
[Info][Imprecise] Invalidating expressions: & return_value_fflush$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2373:3-2373:63)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2357:5-2357:62)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2357:5-2357:62)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2403:5-2403:32)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2401:6-2401:58)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2403:5-2403:32)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2410:5-2410:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2401:6-2401:58)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2403:5-2403:32)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2846:5-2846:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2410:5-2410:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2401:6-2401:58)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2403:5-2403:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2410:5-2410:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2401:6-2401:58)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2403:5-2403:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2410:5-2410:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2401:6-2401:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2410:5-2410:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2401:6-2401:58)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2403:5-2403:32)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3049:3-3049:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2766:11-2766:91)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2760:9-2760:76)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2818:6-2818:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2822:3-2822:56)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2823:4-2823:36)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2741:5-2741:84)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3107:10-3107:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3080:6-3080:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3088:7-3088:15)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3090:6-3090:68)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3095:7-3095:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2793:5-2793:25)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2869:3-2869:41)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2870:3-2870:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2875:3-2875:92)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2875:3-2875:92)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2875:3-2875:92)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2886:6-2886:35)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2895:5-2895:35)
[Info][Imprecise] Invalidating expressions: & fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2392:3-2392:23)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2394:5-2394:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2272:3-2272:25)
[Info][Imprecise] Invalidating expressions: & return_value_strerror$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2241:5-2241:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2246:3-2246:37)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2246:3-2246:37)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2312:3-2312:41)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2312:3-2312:41)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2342:9-2342:24)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2345:9-2345:24)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2349:7-2349:31)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2349:7-2349:31)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2349:7-2349:31)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp, (char * __restrict  )((char *)((void *)0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2910:5-2910:37)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )*fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )*fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2924:7-2924:95)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2945:5-2945:44)
[Info][Imprecise] Invalidating expressions: fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2366:3-2366:35)
[Info][Unsound] Unknown address in fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2366:3-2366:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2366:3-2366:35)
[Info][Imprecise] Invalidating expressions: & return_value_ferror$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2366:3-2366:35)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2368:5-2368:46)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2945:5-2945:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2945:5-2945:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2945:5-2945:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2945:5-2945:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2945:5-2945:44)
[Info][Imprecise] Invalidating expressions: stdout (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2948:3-2948:17)
[Info][Unsound] Unknown address in stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2948:3-2948:17)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2948:3-2948:17)
[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/tee-2.i:3170:5-3170: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/tee-2.i:3170:5-3170: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/tee-2.i:3170:5-3170: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/tee-2.i:3170:5-3170: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/tee-2.i:3170:5-3170: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/tee-2.i:3170:5-3170: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/tee-2.i:3170:5-3170: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/tee-2.i:3170:5-3170: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/tee-2.i:3170:5-3170: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/tee-2.i:3170:5-3170: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/tee-2.i:3170:5-3170: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/tee-2.i:3170:5-3170: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/tee-2.i:3170:5-3170:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:22:1-22:169)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:989:1-993:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:994:1-998:1)
[Warning][Deadcode] Function 'bb_perror_msg_and_die' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2249:1-2265:1)
[Warning][Deadcode] Function 'fflush_stdout_and_exit' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2376:1-2388:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2855:1-2857:1)
[Warning][Deadcode] Function 'xfunc_die' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2963:1-2972:1)
[Warning][Deadcode] Function 'sleep' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3058:1-3062:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3064:1-3074:1)
[Warning][Deadcode] Function 'bb_verror_msg' has dead code:
  on line 2294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2294-2294)
  on line 2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2296-2296)
  on lines 2324..2327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2324-2327)
  on line 2360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2360-2360)
[Warning][Deadcode] Function 'getopt32' has dead code:
  on lines 2477..2479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2477-2479)
  on lines 2482..2484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2482-2484)
  on lines 2487..2491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2487-2491)
  on lines 2494..2495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2494-2495)
  on line 2497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2497-2497)
  on lines 2499..2507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2499-2507)
  on lines 2509..2511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2509-2511)
  on line 2513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2513-2513)
  on lines 2515..2517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2515-2517)
  on line 2519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2519-2519)
  on lines 2521..2525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2521-2525)
  on line 2530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2530-2530)
  on line 2540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2540-2540)
  on line 2547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2547-2547)
  on lines 2549..2550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2549-2550)
  on line 2552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2552-2552)
  on line 2554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2554-2554)
  on line 2561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2561-2561)
  on lines 2564..2565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2564-2565)
  on line 2568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2568-2568)
  on line 2570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2570-2570)
  on line 2572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2572-2572)
  on line 2579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2579-2579)
  on lines 2581..2582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2581-2582)
  on line 2585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2585-2585)
  on lines 2588..2589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2588-2589)
  on line 2592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2592-2592)
  on lines 2594..2596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2594-2596)
  on lines 2600..2602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2600-2602)
  on line 2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2604-2604)
  on line 2607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2607-2607)
  on line 2609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2609-2609)
  on line 2611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2611-2611)
  on line 2617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2617-2617)
  on lines 2619..2620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2619-2620)
  on lines 2622..2623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2622-2623)
  on lines 2625..2626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2625-2626)
  on line 2632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2632-2632)
  on line 2634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2634-2634)
  on line 2641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2641-2641)
  on line 2644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2644-2644)
  on lines 2646..2647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2646-2647)
  on lines 2649..2650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2649-2650)
  on lines 2652..2654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2652-2654)
  on line 2660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2660-2660)
  on lines 2662..2663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2662-2663)
  on lines 2665..2668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2665-2668)
  on lines 2670..2671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2670-2671)
  on lines 2673..2674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2673-2674)
  on lines 2676..2677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2676-2677)
  on line 2679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2679-2679)
  on lines 2681..2682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2681-2682)
  on line 2684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2684-2684)
  on lines 2688..2690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2688-2690)
  on line 2692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2692-2692)
  on line 2696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2696-2696)
  on line 2698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2698-2698)
  on line 2710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2710-2710)
  on lines 2716..2717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2716-2717)
  on line 2719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2719-2719)
  on line 2721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2721-2721)
  on line 2725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2725-2725)
  on lines 2727..2731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2727-2731)
  on line 2734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2734-2734)
  on line 2796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2796-2796)
[Warning][Deadcode] Function 'xmalloc' has dead code:
  on lines 2979..2980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2979-2980)
[Warning][Deadcode] Function 'xstrtou_range_sfx' has dead code:
  on line 3016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3016-3016)
  on lines 3021..3023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3021-3023)
  on line 3025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3025-3025)
  on line 3027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3027-3027)
  on line 3050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3050-3050)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 359
  dead: 172 (36 in uncalled functions)
  total lines: 531
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition 's < tmp' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3123:6-3123:41)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition 's < tmp' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3123:6-3123:41)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition 's < tmp' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3123:6-3123:41)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition 's < tmp' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3123:6-3123:41)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2922:11-2922:19)
[Warning][Deadcode][CWE-571] condition 's < tmp' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3123:6-3123:41)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2930:9-2930:18)
[Warning][Deadcode][CWE-570] condition '! ((6 & spec_flgs) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2714:6-2714:29)
[Warning][Deadcode][CWE-571] condition '(flags & requires) == 0u' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2784:7-2784:30)
[Warning][Deadcode][CWE-571] condition 'requires == 0u' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2786:8-2786:22)
[Warning][Deadcode][CWE-570] condition 'max_arg >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2794:8-2794:20)
[Warning][Deadcode][CWE-571] condition 'i < result_buffer_size' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3130:9-3130:29)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2537:9-2537:17)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )s == (unsigned long )((unsigned char const   *)((void *)0)))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2539:8-2539:52)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(int )tmp_if_expr$7 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2543:8-2543:33)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-570] condition '(unsigned long )ptr == (unsigned long )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2977:6-2977:24)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )suffixes == (unsigned long )((struct suffix_mult *)((void *)0)))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3015:12-3015:62)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[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/tee-2.i:3150:6-3150:25)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[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/tee-2.i:3150:6-3150: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/tee-2.i:3150:6-3150:25)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[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/tee-2.i:3150:6-3150:25)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[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/tee-2.i:3150:6-3150:25)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[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/tee-2.i:3150:6-3150:25)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[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/tee-2.i:3150:6-3150:25)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[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/tee-2.i:3150:6-3150:25)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-570] condition '(int )logmode == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2293:6-2293:30)
[Warning][Deadcode][CWE-570] condition '(unsigned long )s == (unsigned long )((char const   *)((void *)0))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2295:6-2295:38)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[Warning][Deadcode][CWE-571] condition 'r >= lower' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:3035:14-3035: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/tee-2.i:3165:8-3165:27)
[Warning][Deadcode][CWE-570] condition '(unsigned long )msg1 == (unsigned long )((char *)((void *)0))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2322:6-2322:35)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2467:13-2467:22)
[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/tee-2.i:3165:8-3165:27)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )applet_long_options == (unsigned long )((char const   *)((void *)0)))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2473:6-2473:59)
[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/tee-2.i:3165:8-3165: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/tee-2.i:3165:8-3165: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/tee-2.i:3165:8-3165:27)
[Warning][Deadcode][CWE-571] condition '! ((1 & (int )logmode) == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2354:6-2354:39)
[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/tee-2.i:3165:8-3165:27)
[Warning][Deadcode][CWE-570] condition '! ((2 & (int )logmode) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2359:6-2359:39)
[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/tee-2.i:3165:8-3165: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/tee-2.i:3165:8-3165:27)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2773:9-2773:18)
[Warning][Deadcode][CWE-570] condition '! (total == 0l)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i:2406:10-2406: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/tee-2.i:3165:8-3165: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/tee-2.i:3165:8-3165: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/tee-2.i:3165:8-3165: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/tee-2.i:3165:8-3165: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/tee-2.i:3165:8-3165: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/tee-2.i:3165:8-3165: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/tee-2.i:3165:8-3165: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/tee-2.i:3165:8-3165:27)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
