./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/wc-1.i


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2425:3-2436:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2458:3-2459:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2485:7-2491:22 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2503:5-2509:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2516:5-2533:20 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2540:9-2543:9 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2625:13-2628:13 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2713:25-2719:23 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2741:5-2760:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2770:5-2773:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2799:3-2808:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:3-2856:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2891:3-2899:35 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2957:7-3016:7 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3025:7-3040:7 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3121:11-3135:11 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3177:3-3178:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3179:3-3180:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3231:3-3232:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3238:3-3244:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3258:3-3259:34 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3273:5-3274:42 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3268:3-3275:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3277:3-3278: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"
[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/wc-1.i:3265:8-3265:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3265:8-3265:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3265:8-3265:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3266:8-3266:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3266:8-3266:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3266:8-3266:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3274:7-3274:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3274:7-3274:42)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2994:14-2994:49)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2994:14-2994:49)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2984:12-2984:48)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2984:12-2984:48)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2986:11-2986:33)
[Info][Imprecise] Invalidating expressions: & s (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2845:5-2845:23)
[Info][Imprecise] Invalidating expressions: & s (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2847:7-2847:27)
[Info][Imprecise] Invalidating expressions: & s (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2849:7-2849:23)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2850:5-2850:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2458:6-2458:82)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2480:5-2480:47)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2484:7-2484:68)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2780:7-2780:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2780:7-2780:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2794:13-2794:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2789:11-2789:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3059:3-3059:92)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3065:3-3065:114)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3095:6-3095:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3098:5-3098:99)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3105:19-3105:73)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3105:19-3105:73)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3114:5-3114:35)
[Info][Unsound] Unknown address in {&e} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3114:5-3114:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3114:5-3114:35)
[Info][Imprecise] Invalidating expressions: (char ** __restrict  )end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2279:3-2279:25)
[Info][Imprecise] Invalidating expressions: & v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2279:3-2279:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3136:12-3136:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3147:11-3147:141)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2231:3-2231:49)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2299:3-2299:29)
[Info][Unsound] Unknown address in {&msg} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2299:3-2299:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2299:3-2299:29)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2304:3-2304:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2304:3-2304: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/wc-1.i:2319:3-2319:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2319:3-2319:116)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2319:3-2319:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2334:5-2334:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2335:5-2335:29)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2337:5-2337:54)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2338:5-2338:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2354:5-2354:29)
[Info][Imprecise] Invalidating expressions: (struct _IO_FILE *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2382:3-2382:63)
[Info][Imprecise] Invalidating expressions: & return_value_fflush$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2382:3-2382:63)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2359:5-2359:62)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2359:5-2359:62)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2427:5-2427:32)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2425:6-2425:58)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2427:5-2427:32)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2434:5-2434:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2425:6-2425:58)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2427:5-2427:32)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2893:5-2893:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2434:5-2434:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2425:6-2425:58)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2427:5-2427:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2434:5-2434:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2425:6-2425:58)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2427:5-2427:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2434:5-2434:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2425:6-2425:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2434:5-2434:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2425:6-2425:58)
[Info][Unsound] Unknown value in {&(alloc@sid:76)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2427:5-2427:32)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3154:3-3154:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2790:11-2790:91)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2784:9-2784:76)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2855:6-2855:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2859:3-2859:56)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2860:4-2860:36)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2765:5-2765:84)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3215:10-3215:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3188:6-3188:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3196:7-3196:15)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3198:6-3198:68)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3203:7-3203:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2817:5-2817:25)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2929:9-2929:53)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2948:5-2948:30)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2949:5-2949:32)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2417:7-2417:38)
[Info][Imprecise] Invalidating expressions: & fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2401:3-2401:23)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2403:5-2403:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2274:3-2274:25)
[Info][Imprecise] Invalidating expressions: & return_value_strerror$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2243:5-2243:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2248:3-2248:37)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2248:3-2248:37)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2314:3-2314:41)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2319:3-2319:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2344:9-2344:24)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2347:9-2347:24)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2351:7-2351:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2960:9-2960:24)
[Info][Imprecise] Invalidating expressions: stream (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3164:10-3164:23)
[Info][Unsound] Unknown address in stream has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3164:10-3164:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3164:10-3164:23)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3164:10-3164:23)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2972:9-2972:69)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2982:11-2982:71)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2984:12-2984:48)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2984:12-2984:48)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2994:14-2994:49)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2994:14-2994:49)
[Info][Imprecise] Invalidating expressions: fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2964:11-2964:43)
[Info][Unsound] Unknown address in fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2964:11-2964:43)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2964:11-2964:43)
[Info][Imprecise] Invalidating expressions: & return_value_ferror$2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2964:11-2964:43)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2967:13-2967:38)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3005:17-3005:77)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2960:9-2960:24)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2972:9-2972:69)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2982:11-2982:71)
[Info][Imprecise] Invalidating expressions: fp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2964:11-2964:43)
[Info][Unsound] Unknown address in fp has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2964:11-2964:43)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2964:11-2964:43)
[Info][Imprecise] Invalidating expressions: & return_value_ferror$2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2964:11-2964:43)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2967:13-2967:38)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3005:17-3005:77)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2997:15-2997:70)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3012:9-3012:88)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3017:7-3017:30)
[Info][Imprecise] Invalidating expressions: f (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2368:3-2368:14)
[Info][Unsound] Unknown address in f has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2368:3-2368:14)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2368:3-2368:14)
[Info][Imprecise] Invalidating expressions: & r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2368:3-2368:14)
[Info][Imprecise] Invalidating expressions: f (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2374:5-2374:36)
[Info][Unsound] Unknown address in f has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2374:5-2374:36)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2374:5-2374:36)
[Info][Imprecise] Invalidating expressions: & return_value_fclose$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2374:5-2374:36)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3020:7-3020:91)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3036:9-3036:94)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3036:9-3036:94)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3036:9-3036:94)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3036:9-3036:94)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3036:9-3036:94)
[Info][Imprecise] Invalidating expressions: stdout (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3053:3-3053:17)
[Info][Unsound] Unknown address in stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3053:3-3053:17)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3053:3-3053:17)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3278:5-3278: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/wc-1.i:3278:5-3278: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/wc-1.i:3278:5-3278: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/wc-1.i:3278:5-3278: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/wc-1.i:3278:5-3278: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/wc-1.i:3278:5-3278: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/wc-1.i:3278:5-3278: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/wc-1.i:3278:5-3278: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/wc-1.i:3278:5-3278: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/wc-1.i:3278:5-3278: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/wc-1.i:3278:5-3278: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/wc-1.i:3278:5-3278: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/wc-1.i:3278:5-3278:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.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/wc-1.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/wc-1.i:994:1-998:1)
[Warning][Deadcode] Function 'bb_perror_msg_and_die' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2251:1-2267:1)
[Warning][Deadcode] Function 'fflush_stdout_and_exit' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2385:1-2397:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2902:1-2904:1)
[Warning][Deadcode] Function 'xfunc_die' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3068:1-3077:1)
[Warning][Deadcode] Function 'sleep' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3166:1-3170:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3172:1-3182:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3217:1-3225:1)
[Warning][Deadcode] Function '__main' has dead code:
  on line 3035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3035-3035)
[Warning][Deadcode] Function 'bb_verror_msg' has dead code:
  on line 2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2296-2296)
  on line 2298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2298-2298)
  on lines 2326..2329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2326-2329)
  on line 2362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2362-2362)
[Warning][Deadcode] Function 'getopt32' has dead code:
  on lines 2501..2503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2501-2503)
  on lines 2506..2508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2506-2508)
  on lines 2511..2515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2511-2515)
  on lines 2518..2519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2518-2519)
  on line 2521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2521-2521)
  on lines 2523..2531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2523-2531)
  on lines 2533..2535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2533-2535)
  on line 2537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2537-2537)
  on lines 2539..2541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2539-2541)
  on line 2543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2543-2543)
  on lines 2545..2549 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2545-2549)
  on line 2554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2554-2554)
  on line 2564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2564-2564)
  on line 2571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2571-2571)
  on lines 2573..2574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2573-2574)
  on line 2576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2576-2576)
  on line 2578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2578-2578)
  on line 2585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2585-2585)
  on lines 2588..2589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2588-2589)
  on line 2592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2592-2592)
  on line 2594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2594-2594)
  on line 2596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2596-2596)
  on line 2603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2603-2603)
  on lines 2605..2606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2605-2606)
  on line 2609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2609-2609)
  on lines 2612..2613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2612-2613)
  on line 2616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2616-2616)
  on lines 2618..2620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2618-2620)
  on lines 2624..2626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2624-2626)
  on line 2628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2628-2628)
  on line 2631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2631-2631)
  on line 2633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2633-2633)
  on line 2635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2635-2635)
  on line 2641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2641-2641)
  on lines 2643..2644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2643-2644)
  on lines 2646..2647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2646-2647)
  on lines 2649..2650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2649-2650)
  on line 2656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2656-2656)
  on line 2658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2658-2658)
  on line 2665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2665-2665)
  on line 2668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2668-2668)
  on lines 2670..2671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2670-2671)
  on lines 2673..2674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2673-2674)
  on lines 2676..2678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2676-2678)
  on line 2684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2684-2684)
  on lines 2686..2687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2686-2687)
  on lines 2689..2692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2689-2692)
  on lines 2694..2695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2694-2695)
  on lines 2697..2698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2697-2698)
  on lines 2700..2701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2700-2701)
  on line 2703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2703-2703)
  on lines 2705..2706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2705-2706)
  on line 2708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2708-2708)
  on lines 2712..2714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2712-2714)
  on line 2716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2716-2716)
  on line 2720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2720-2720)
  on line 2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2722-2722)
  on line 2734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2734-2734)
  on lines 2740..2741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2740-2741)
  on line 2743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2743-2743)
  on line 2745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2745-2745)
  on line 2749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2749-2749)
  on lines 2751..2755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2751-2755)
  on line 2758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2758-2758)
  on line 2820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2820-2820)
[Warning][Deadcode] Function 'xmalloc' has dead code:
  on lines 3084..3085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3084-3085)
[Warning][Deadcode] Function 'xstrtou_range_sfx' has dead code:
  on line 3121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3121-3121)
  on lines 3126..3128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3126-3128)
  on line 3130 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3130-3130)
  on line 3132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3132-3132)
  on line 3155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3155-3155)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 410
  dead: 179 (42 in uncalled functions)
  total lines: 589
[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/wc-1.i:3273:8-3273: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/wc-1.i:2957:13-2957:21)
[Warning][Deadcode][CWE-570] condition '! (counts[4l] >= linepos)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3002:18-3002:42)
[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/wc-1.i:2957:13-2957:21)
[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/wc-1.i:3231:6-3231: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/wc-1.i:3231:6-3231: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/wc-1.i:3025:13-3025:21)
[Warning][Deadcode][CWE-571] condition '(long )u < 5l' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3032:12-3032:35)
[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/wc-1.i:3231:6-3231:41)
[Warning][Deadcode][CWE-570] condition '! (u < 5u)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3038:12-3038:21)
[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/wc-1.i:3025:13-3025:21)
[Warning][Deadcode][CWE-571] condition '(long )u < 5l' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3032:12-3032:35)
[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/wc-1.i:3231:6-3231:41)
[Warning][Deadcode][CWE-570] condition '! (u < 5u)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3038:12-3038:21)
[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/wc-1.i:3025:13-3025:21)
[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/wc-1.i:3231:6-3231:41)
[Warning][Deadcode][CWE-571] condition '(long )u < 5l' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3032:12-3032:35)
[Warning][Deadcode][CWE-570] condition '! (u < 5u)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3038:12-3038:21)
[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/wc-1.i:3025:13-3025:21)
[Warning][Deadcode][CWE-571] condition '(long )u < 5l' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3032:12-3032:35)
[Warning][Deadcode][CWE-570] condition '! (u < 5u)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3038:12-3038:21)
[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/wc-1.i:3025:13-3025:21)
[Warning][Deadcode][CWE-571] condition '(long )u < 5l' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3032:12-3032:35)
[Warning][Deadcode][CWE-570] condition '! ((6 & spec_flgs) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2738:6-2738:29)
[Warning][Deadcode][CWE-571] condition '! (u < 5u)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3038:12-3038:21)
[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/wc-1.i:3238:9-3238:29)
[Warning][Deadcode][CWE-571] condition '(flags & requires) == 0u' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2808:7-2808:30)
[Warning][Deadcode][CWE-571] condition 'requires == 0u' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2810:8-2810:22)
[Warning][Deadcode][CWE-570] condition 'max_arg >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2818:8-2818:20)
[Warning][Deadcode][CWE-571] condition '(int )unicode_status == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2842:6-2842:37)
[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/wc-1.i:3044:9-3044:18)
[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/wc-1.i:2491:13-2491: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/wc-1.i:2491:13-2491: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/wc-1.i:2491:13-2491: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/wc-1.i:2561:9-2561: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/wc-1.i:2563:8-2563: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/wc-1.i:2491:13-2491: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/wc-1.i:3082:6-3082:24)
[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/wc-1.i:2567:8-2567: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/wc-1.i:2491:13-2491: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/wc-1.i:2491:13-2491: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/wc-1.i:2491:13-2491: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/wc-1.i:2491:13-2491: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/wc-1.i:2491:13-2491: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/wc-1.i:2491:13-2491: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/wc-1.i:3120:12-3120: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/wc-1.i:2491:13-2491: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/wc-1.i:3258:6-3258: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/wc-1.i:2491:13-2491: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/wc-1.i:3258:6-3258: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/wc-1.i:2491:13-2491: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/wc-1.i:3258:6-3258: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/wc-1.i:2491:13-2491: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/wc-1.i:3258:6-3258: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/wc-1.i:2491:13-2491: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/wc-1.i:3258:6-3258: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/wc-1.i:2491:13-2491: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/wc-1.i:3258:6-3258: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/wc-1.i:2491:13-2491: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/wc-1.i:3258:6-3258:25)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3258:6-3258: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/wc-1.i:2491:13-2491: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/wc-1.i:2491:13-2491:22)
[Warning][Deadcode][CWE-570] condition '(int )logmode == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2295:6-2295: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/wc-1.i:2297:6-2297:38)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2491:13-2491: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/wc-1.i:2491:13-2491: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/wc-1.i:2491:13-2491: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/wc-1.i:2491:13-2491:22)
[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/wc-1.i:2324:6-2324:35)
[Warning][Deadcode][CWE-571] condition 'r >= lower' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3140:14-3140: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/wc-1.i:2491:13-2491:22)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3273:8-3273: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/wc-1.i:2491:13-2491:22)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3273:8-3273: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/wc-1.i:3273:8-3273: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/wc-1.i:2491:13-2491:22)
[Warning][Deadcode][CWE-571] condition '! ((1 & (int )logmode) == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2356:6-2356:39)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3273:8-3273:27)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )applet_long_options == (unsigned long )((char const   *)((void *)0)))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2497:6-2497:59)
[Warning][Deadcode][CWE-570] condition '! ((2 & (int )logmode) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2361:6-2361:39)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:3273:8-3273: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/wc-1.i:3273:8-3273: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/wc-1.i:3273:8-3273: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/wc-1.i:3273:8-3273: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/wc-1.i:2797:9-2797: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/wc-1.i:3273:8-3273: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/wc-1.i:3273:8-3273:27)
[Warning][Deadcode][CWE-570] condition '! (total == 0l)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/wc-1.i:2430:10-2430: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/wc-1.i:3273:8-3273: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/wc-1.i:3273:8-3273: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/wc-1.i:3273:8-3273: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/wc-1.i:3273:8-3273: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/wc-1.i:3273:8-3273:27)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
