./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/tac-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/tac-2.i:2383:3-2394:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2416:3-2417:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2443:7-2449:22 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2461:5-2467:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2474:5-2491:20 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2498:9-2501:9 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2583:13-2586:13 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2671:25-2677:23 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2699:5-2718:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2728:5-2731:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2757:3-2766:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:3-2811:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2821:3-2829:35 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2850:3-2855:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2870:7-2905:22 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2917:3-2921:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2999:11-3013:11 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3065:3-3066:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3067:3-3068:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:3-3120:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3126:3-3132:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3146:3-3147:34 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3161:5-3162:42 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3156:3-3163:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3165:3-3166: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/tac-2.i:3153:8-3153:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3153:8-3153:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3153:8-3153:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3154:8-3154:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3154:8-3154:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3154:8-3154:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3162:7-3162:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3162:7-3162:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2416:6-2416:82)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2438:5-2438:47)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2442:7-2442:68)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2738:7-2738:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2738:7-2738:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2752:13-2752:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2747:11-2747:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2927:3-2927:92)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2933:3-2933:114)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2973:6-2973:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2976:5-2976:99)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2983:19-2983:73)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2983:19-2983:73)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2992:5-2992:35)
[Info][Unsound] Unknown address in {&e} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2992:5-2992:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2992:5-2992:35)
[Info][Imprecise] Invalidating expressions: (char ** __restrict  )end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2264:3-2264:25)
[Info][Imprecise] Invalidating expressions: & v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2264:3-2264:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3014:12-3014:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3025:11-3025:141)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2233:3-2233:49)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2284:3-2284:29)
[Info][Unsound] Unknown address in {&msg} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2284:3-2284:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2284:3-2284:29)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2289:3-2289:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2289:3-2289: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/tac-2.i:2304:3-2304:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2304:3-2304:116)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2304:3-2304:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2319:5-2319:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2320:5-2320:29)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2322:5-2322:54)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2323:5-2323:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2339:5-2339:29)
[Info][Imprecise] Invalidating expressions: (struct _IO_FILE *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2353:3-2353:63)
[Info][Imprecise] Invalidating expressions: & return_value_fflush$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2353:3-2353:63)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2344:5-2344:62)
[Info][Unsound] Unknown value in {&(alloc@sid:64)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2344:5-2344:62)
[Info][Unsound] Unknown value in {&(alloc@sid:64)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Info][Unsound] Unknown value in {&(alloc@sid:64)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Info][Unsound] Unknown value in {&(alloc@sid:64)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Info][Unsound] Unknown value in {&(alloc@sid:64)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Info][Unsound] Unknown value in {&(alloc@sid:64)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Info][Unsound] Unknown value in {&(alloc@sid:64)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2383:6-2383:58)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2385:5-2385:32)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2823:5-2823:28)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2823:5-2823:28)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2823:5-2823:28)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2823:5-2823:28)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2823:5-2823:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2392:5-2392:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2383:6-2383:58)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2385:5-2385:32)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2823:5-2823:28)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2823:5-2823:28)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2823:5-2823:28)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2823:5-2823:28)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2823:5-2823:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2392:5-2392:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2383:6-2383:58)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2385:5-2385:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2392:5-2392:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2383:6-2383:58)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2385:5-2385:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2392:5-2392:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2383:6-2383:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2392:5-2392:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2383:6-2383:58)
[Info][Unsound] Unknown value in {&(alloc@sid:64)[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/tac-2.i:2385:5-2385:32)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3032:3-3032:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2748:11-2748:91)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2742:9-2742:76)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2810:6-2810:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2814:3-2814:56)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2815:4-2815:36)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2723:5-2723:84)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3103:10-3103:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3076:6-3076:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3084:7-3084:15)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3086:6-3086:68)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3091:7-3091:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2775:5-2775:25)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2863:5-2863:33)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2370:8-2370:38)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2375:7-2375:38)
[Info][Imprecise] Invalidating expressions: & fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2359:3-2359:23)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2361:5-2361:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2259:3-2259:25)
[Info][Imprecise] Invalidating expressions: & return_value_strerror$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2245:5-2245:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2250:3-2250:37)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2250:3-2250:37)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2299:3-2299:41)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2304:3-2304:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2329:9-2329:24)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2332:9-2332:24)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2336:7-2336:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2872:9-2872:24)
[Info][Imprecise] Invalidating expressions: stream (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3052:10-3052:23)
[Info][Unsound] Unknown address in stream has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3052:10-3052:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3052:10-3052:23)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3052:10-3052:23)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2882:11-2882:60)
[Info][Unsound] Unknown value in {&(alloc@sid:2518)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2900:11-2900:44)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2804:3-2804:32)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2805:3-2805:29)
[Info][Unsound] Unknown value in {&(alloc@sid:2518)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2805:3-2805:29)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2900:11-2900:44)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2900:11-2900:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2872:9-2872:24)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2877:13-2877:133)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2881:11-2881:20)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2882:11-2882:60)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2882:11-2882:60)
[Info][Unsound] Unknown value in {&(alloc@sid:2518)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2900:11-2900:44)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2900:11-2900:44)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2900:11-2900:44)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3039:5-3039:36)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3039:5-3039:36)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2382:19-2382:45)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:26:141-26:144)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3138:8-3138:36)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3138:8-3138:36)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3139:3-3139:59)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3139:3-3139:59)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3139:3-3139:59)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:10:1-10:1)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3140:10-3140:13)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2827:7-2827:29)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2827:7-2827:29)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2827:7-2827:29)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2827:7-2827:29)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2823:5-2823:28)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2827:7-2827:29)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2825:7-2825:90)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2830:10-2830:11)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2390:14-2390:16)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2392:5-2392:23)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2393:5-2393:49)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2383:6-2383:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2389:16-2389:21)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2390:14-2390:16)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2392:5-2392:23)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2393:5-2393:49)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2383:6-2383:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2389:16-2389:21)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2390:14-2390:16)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2392:5-2392:23)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2393:5-2393:49)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2383:6-2383:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2389:16-2389:21)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2390:14-2390:16)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2392:5-2392:23)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2393:5-2393:49)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2383:6-2383:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2389:16-2389:21)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2390:14-2390:16)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2392:5-2392:23)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2393:5-2393:49)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2383:6-2383:58)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2392:5-2392:23)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2393:5-2393:49)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2383:6-2383:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2385:5-2385:32)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2389:16-2389:21)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2390:14-2390:16)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2395:10-2395:15)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3040:8-3040:43)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3041:7-3041:42)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2233:3-2233:49)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2284:3-2284:29)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3118:7-3118:20)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:14-3119:19)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:6-3119:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:63-3119:76)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:14-3119:19)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:6-3119:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:63-3119:76)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:14-3119:19)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:6-3119:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:63-3119:76)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:14-3119:19)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:6-3119:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:63-3119:76)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:14-3119:19)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:6-3119:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:63-3119:76)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:14-3119:19)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:6-3119:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:63-3119:76)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:14-3119:19)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:14-3119:19)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:6-3119:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3119:63-3119:76)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3120:19-3120:45)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3120:19-3120:45)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3120:19-3120:45)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3120:73-3120:84)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3120:73-3120:84)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:22:136-22:139)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3121:7-3121:51)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3121:7-3121:51)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3123:12-3123:14)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3124:3-3124:36)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3124:3-3124:36)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3125:7-3125:12)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:20:141-20:144)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3128:6-3128:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3131:5-3131:8)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3128:6-3128:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3131:5-3131:8)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3128:6-3128:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3131:5-3131:8)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3128:6-3128:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3131:5-3131:8)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3128:6-3128:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3131:5-3131:8)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3128:6-3128:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3131:5-3131:8)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3128:6-3128:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3131:5-3131:8)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3128:6-3128:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3131:5-3131:8)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3128:6-3128:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3131:5-3131:8)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3133:3-3133:44)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3134:10-3134:11)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2286:5-2286:11)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2288:3-2288:44)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2289:3-2289:74)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2298:5-2298:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2299:3-2299:41)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2301:3-2301:40)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2302:3-2302:49)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2304:3-2304:116)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2305:3-2305:40)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2318:5-2318:15)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2320:5-2320:29)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2322:5-2322:54)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2323:5-2323:54)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2339:5-2339:29)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2353:3-2353:63)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2354:10-2354:31)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2344:5-2344:62)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2349:1-2349:1)
[Warning][Unknown] lval (& line)->buf points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3043:1-3043:1)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2920:5-2920:70)
[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/tac-2.i:3166:5-3166: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/tac-2.i:3166:5-3166: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/tac-2.i:3166:5-3166: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/tac-2.i:3166:5-3166: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/tac-2.i:3166:5-3166: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/tac-2.i:3166:5-3166: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/tac-2.i:3166:5-3166: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/tac-2.i:3166:5-3166: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/tac-2.i:3166:5-3166: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/tac-2.i:3166:5-3166: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/tac-2.i:3166:5-3166: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/tac-2.i:3166:5-3166: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/tac-2.i:3166:5-3166:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-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/tac-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/tac-2.i:994:1-998:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2832:1-2834:1)
[Warning][Deadcode] Function 'xfunc_die' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2936:1-2945:1)
[Warning][Deadcode] Function 'sleep' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3054:1-3058:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3060:1-3070:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3105:1-3113:1)
[Warning][Deadcode] Function '__main' has dead code:
  on line 2908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2908-2908)
  on lines 2910..2911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2910-2911)
[Warning][Deadcode] Function 'bb_verror_msg' has dead code:
  on line 2281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2281-2281)
  on line 2283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2283-2283)
  on lines 2311..2314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2311-2314)
  on line 2347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2347-2347)
[Warning][Deadcode] Function 'getopt32' has dead code:
  on lines 2459..2461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2459-2461)
  on lines 2464..2466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2464-2466)
  on lines 2469..2473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2469-2473)
  on lines 2476..2477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2476-2477)
  on line 2479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2479-2479)
  on lines 2481..2489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2481-2489)
  on lines 2491..2493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2491-2493)
  on line 2495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2495-2495)
  on lines 2497..2499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2497-2499)
  on line 2501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2501-2501)
  on lines 2503..2507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2503-2507)
  on line 2512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2512-2512)
  on line 2522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2522-2522)
  on line 2529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2529-2529)
  on lines 2531..2532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2531-2532)
  on line 2534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2534-2534)
  on line 2536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2536-2536)
  on line 2543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2543-2543)
  on lines 2546..2547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2546-2547)
  on line 2550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2550-2550)
  on line 2552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2552-2552)
  on line 2554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2554-2554)
  on line 2561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2561-2561)
  on lines 2563..2564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2563-2564)
  on line 2567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2567-2567)
  on lines 2570..2571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2570-2571)
  on line 2574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2574-2574)
  on lines 2576..2578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2576-2578)
  on lines 2582..2584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2582-2584)
  on line 2586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2586-2586)
  on line 2589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2589-2589)
  on line 2591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2591-2591)
  on line 2593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2593-2593)
  on line 2599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2599-2599)
  on lines 2601..2602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2601-2602)
  on lines 2604..2605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2604-2605)
  on lines 2607..2608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2607-2608)
  on line 2614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2614-2614)
  on line 2616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2616-2616)
  on line 2623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2623-2623)
  on line 2626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2626-2626)
  on lines 2628..2629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2628-2629)
  on lines 2631..2632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2631-2632)
  on lines 2634..2636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2634-2636)
  on line 2642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2642-2642)
  on lines 2644..2645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2644-2645)
  on lines 2647..2650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2647-2650)
  on lines 2652..2653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2652-2653)
  on lines 2655..2656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2655-2656)
  on lines 2658..2659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2658-2659)
  on line 2661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2661-2661)
  on lines 2663..2664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2663-2664)
  on line 2666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2666-2666)
  on lines 2670..2672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2670-2672)
  on line 2674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2674-2674)
  on line 2678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2678-2678)
  on line 2680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2680-2680)
  on line 2692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2692-2692)
  on lines 2698..2699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2698-2699)
  on line 2701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2701-2701)
  on line 2703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2703-2703)
  on line 2707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2707-2707)
  on lines 2709..2713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2709-2713)
  on line 2716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2716-2716)
  on line 2778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2778-2778)
[Warning][Deadcode] Function 'xmalloc' has dead code:
  on lines 2952..2953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2952-2953)
[Warning][Deadcode] Function 'xrealloc' has dead code:
  on lines 2962..2963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2962-2963)
[Warning][Deadcode] Function 'xstrtou_range_sfx' has dead code:
  on line 2999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2999-2999)
  on lines 3004..3006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3004-3006)
  on line 3008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3008-3008)
  on line 3010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3010-3010)
  on line 3033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3033-3033)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 359
  dead: 168 (27 in uncalled functions)
  total lines: 527
[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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:3161:8-3161: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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:2850:9-2850:17)
[Warning][Deadcode][CWE-571] condition '(127 & i) == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2875:15-2875:28)
[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/tac-2.i:3119:6-3119:41)
[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/tac-2.i:3119:6-3119:41)
[Warning][Deadcode][CWE-570] condition '! ((6 & spec_flgs) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2696:6-2696:29)
[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/tac-2.i:3119:6-3119:41)
[Warning][Deadcode][CWE-571] condition '(flags & requires) == 0u' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2766:7-2766:30)
[Warning][Deadcode][CWE-570] condition '! (*bb_errno == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2906:10-2906:27)
[Warning][Deadcode][CWE-571] condition 'requires == 0u' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2768:8-2768:22)
[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/tac-2.i:3119:6-3119:41)
[Warning][Deadcode][CWE-570] condition 'max_arg >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2776:8-2776:20)
[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/tac-2.i:3119:6-3119: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2519:9-2519: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/tac-2.i:2521:8-2521: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/tac-2.i:2449:13-2449:22)
[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/tac-2.i:3126:9-3126:29)
[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/tac-2.i:2525:8-2525: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2950:6-2950: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/tac-2.i:2449:13-2449: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/tac-2.i:2960:6-2960: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:2998:12-2998: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/tac-2.i:2449:13-2449: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/tac-2.i:2449:13-2449: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/tac-2.i:3146:6-3146: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/tac-2.i:2449:13-2449: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/tac-2.i:3146:6-3146: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/tac-2.i:2449:13-2449: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/tac-2.i:3146:6-3146:25)
[Warning][Deadcode][CWE-570] condition '(int )logmode == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2280:6-2280: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/tac-2.i:2282:6-2282:38)
[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/tac-2.i:3146:6-3146: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/tac-2.i:2449:13-2449: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/tac-2.i:3146:6-3146: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/tac-2.i:2449:13-2449: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/tac-2.i:3146:6-3146: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/tac-2.i:2449:13-2449: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/tac-2.i:3146:6-3146:25)
[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/tac-2.i:2309:6-2309:35)
[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/tac-2.i:3146:6-3146: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/tac-2.i:2449:13-2449:22)
[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/tac-2.i:2455:6-2455:59)
[Warning][Deadcode][CWE-571] condition '! ((1 & (int )logmode) == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2341:6-2341:39)
[Warning][Deadcode][CWE-570] condition '! ((2 & (int )logmode) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2346:6-2346:39)
[Warning][Deadcode][CWE-571] condition 'r >= lower' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:3018:14-3018: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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:3161:8-3161: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/tac-2.i:2755:9-2755:18)
[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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[Warning][Deadcode][CWE-570] condition '! (total == 0l)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tac-2.i:2388:10-2388: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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:3161:8-3161: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/tac-2.i:2850:9-2850:17)
[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/tac-2.i:3161:8-3161:27)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
