./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/uname-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/uname-1.i:2385:3-2396:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2418:3-2419:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2445:7-2451:22 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2463:5-2469:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2476:5-2493:20 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2500:9-2503:9 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2585:13-2588:13 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2673:25-2679:23 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2701:5-2720:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2730:5-2733:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2759:3-2768:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:3-2803:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2813:3-2821:35 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2852:3-2867:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2937:11-2951:11 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2989:2-2990:45 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2992:2-2993:46 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2995:2-2996:45 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2998:2-2999:45 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3001:2-3002:45 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3004:2-3005:48 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3015:3-3016:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3017:3-3018:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3069:3-3070:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3076:3-3082:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3096:3-3097:34 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3111:5-3112:42 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3106:3-3113:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3115:3-3116: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/uname-1.i:3103:8-3103:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3103:8-3103:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3103:8-3103:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3104:8-3104:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3104:8-3104:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3104:8-3104:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3112:7-3112:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3112:7-3112:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2418:6-2418:82)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2440:5-2440:47)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2467:7-2467:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2468:7-2468:25)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2475:5-2475:33)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2475:5-2475:33)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2478:7-2478:25)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2484:7-2484:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2484:7-2484:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2484:7-2484:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2484:7-2484:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2484:7-2484:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2484:7-2484:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2491:7-2491:17)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2506:9-2506:51)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2508:11-2508:72)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2740:7-2740:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2740:7-2740:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2754:13-2754:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2749:11-2749:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2875:3-2875:92)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2881:3-2881:114)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2911:6-2911:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2914:5-2914:99)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2921:19-2921:73)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2921:19-2921:73)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2930:5-2930:35)
[Info][Unsound] Unknown address in {&e} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2930:5-2930:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2930:5-2930:35)
[Info][Imprecise] Invalidating expressions: (char ** __restrict  )end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2276:3-2276:25)
[Info][Imprecise] Invalidating expressions: & v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2276:3-2276:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2952:12-2952:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2963:11-2963:141)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2242:3-2242:49)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2296:3-2296:29)
[Info][Unsound] Unknown address in {&msg} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2296:3-2296:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2296:3-2296:29)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2301:3-2301:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2301:3-2301: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/uname-1.i:2316:3-2316:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2316:3-2316:116)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2316:3-2316:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2331:5-2331:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2332:5-2332:29)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2334:5-2334:54)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2335:5-2335:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2351:5-2351:29)
[Info][Imprecise] Invalidating expressions: (struct _IO_FILE *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2365:3-2365:63)
[Info][Imprecise] Invalidating expressions: & return_value_fflush$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2365:3-2365:63)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2356:5-2356: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/uname-1.i:2356:5-2356: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/uname-1.i:2387:5-2387: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/uname-1.i:2815:5-2815: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/uname-1.i:2815:5-2815: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/uname-1.i:2815:5-2815: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/uname-1.i:2815:5-2815: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/uname-1.i:2815:5-2815:28)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2385:6-2385: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/uname-1.i:2387:5-2387: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/uname-1.i:2815:5-2815: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/uname-1.i:2815:5-2815: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/uname-1.i:2815:5-2815: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/uname-1.i:2815:5-2815: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/uname-1.i:2815:5-2815:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2394:5-2394:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2385:6-2385: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/uname-1.i:2387:5-2387: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/uname-1.i:2815:5-2815: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/uname-1.i:2815:5-2815: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/uname-1.i:2815:5-2815: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/uname-1.i:2815:5-2815: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/uname-1.i:2815:5-2815:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2394:5-2394:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2385:6-2385: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/uname-1.i:2387:5-2387:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2394:5-2394:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2385:6-2385: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/uname-1.i:2387:5-2387:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2394:5-2394:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2385:6-2385:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2394:5-2394:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2385:6-2385: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/uname-1.i:2387:5-2387:32)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2970:3-2970:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2750:11-2750:91)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2744:9-2744:76)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2802:6-2802:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2806:3-2806:56)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2807:4-2807:36)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3026:6-3026:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3034:7-3034:15)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3036:6-3036:68)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3046:10-3046:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2777:5-2777:25)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2864:5-2864:27)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2864:5-2864:27)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2864:5-2864:27)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2864:5-2864:27)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2864:5-2864:27)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2864:5-2864:27)
[Info][Imprecise] Invalidating expressions: & return_value_putchar_unlocked$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2266:3-2266:46)
[Info][Imprecise] Invalidating expressions: stdout (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2869:3-2869:17)
[Info][Unsound] Unknown address in stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2869:3-2869:17)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2869:3-2869: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/uname-1.i:3116:5-3116: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/uname-1.i:3116:5-3116: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/uname-1.i:3116:5-3116: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/uname-1.i:3116:5-3116: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/uname-1.i:3116:5-3116: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/uname-1.i:3116:5-3116: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/uname-1.i:3116:5-3116: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/uname-1.i:3116:5-3116: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/uname-1.i:3116:5-3116: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/uname-1.i:3116:5-3116: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/uname-1.i:3116:5-3116: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/uname-1.i:3116:5-3116: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/uname-1.i:3116:5-3116:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-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/uname-1.i:986:1-990:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:991:1-995:1)
[Warning][Deadcode] Function 'bb_perror_msg_and_die' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2246:1-2262:1)
[Warning][Deadcode] Function 'fflush_stdout_and_exit' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2368:1-2380:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2824:1-2826:1)
[Warning][Deadcode] Function 'xfunc_die' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2884:1-2893:1)
[Warning][Deadcode] Function 'sleep' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2979:1-2983:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3010:1-3020:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3055:1-3063:1)
[Warning][Deadcode] Function 'bb_verror_msg' has dead code:
  on line 2293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2293-2293)
  on line 2295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2295-2295)
  on lines 2306..2307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2306-2307)
  on lines 2323..2326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2323-2326)
  on line 2338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2338-2338)
  on lines 2340..2345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2340-2345)
  on lines 2347..2348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2347-2348)
  on line 2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2359-2359)
[Warning][Deadcode] Function 'getopt' has dead code:
  on line 3038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3038-3038)
  on lines 3040..3041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3040-3041)
  on line 3044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3044-3044)
[Warning][Deadcode] Function 'getopt32' has dead code:
  on line 2426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2426-2426)
  on line 2430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2430-2430)
  on line 2434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2434-2434)
  on line 2444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2444-2444)
  on lines 2447..2448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2447-2448)
  on line 2451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2451-2451)
  on line 2524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2524-2524)
  on line 2531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2531-2531)
  on lines 2533..2534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2533-2534)
  on line 2536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2536-2536)
  on line 2538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2538-2538)
  on line 2545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2545-2545)
  on lines 2548..2549 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2548-2549)
  on line 2552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2552-2552)
  on line 2554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2554-2554)
  on line 2556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2556-2556)
  on line 2563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2563-2563)
  on lines 2565..2566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2565-2566)
  on line 2569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2569-2569)
  on lines 2572..2573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2572-2573)
  on line 2576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2576-2576)
  on lines 2578..2580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2578-2580)
  on lines 2584..2586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2584-2586)
  on line 2588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2588-2588)
  on line 2591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2591-2591)
  on line 2593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2593-2593)
  on line 2595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2595-2595)
  on line 2601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2601-2601)
  on lines 2603..2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2603-2604)
  on lines 2606..2607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2606-2607)
  on lines 2609..2610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2609-2610)
  on line 2616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2616-2616)
  on line 2618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2618-2618)
  on line 2625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2625-2625)
  on line 2628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2628-2628)
  on lines 2630..2631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2630-2631)
  on lines 2633..2634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2633-2634)
  on lines 2636..2638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2636-2638)
  on line 2644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2644-2644)
  on lines 2646..2647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2646-2647)
  on lines 2649..2652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2649-2652)
  on lines 2654..2655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2654-2655)
  on lines 2657..2658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2657-2658)
  on lines 2660..2661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2660-2661)
  on line 2663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2663-2663)
  on lines 2665..2666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2665-2666)
  on line 2668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2668-2668)
  on lines 2672..2674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2672-2674)
  on line 2676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2676-2676)
  on line 2680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2680-2680)
  on line 2682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2682-2682)
  on line 2694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2694-2694)
  on lines 2700..2701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2700-2701)
  on line 2703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2703-2703)
  on line 2705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2705-2705)
  on line 2709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2709-2709)
  on lines 2711..2715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2711-2715)
  on line 2718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2718-2718)
  on line 2780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2780-2780)
[Warning][Deadcode] Function 'xmalloc' has dead code:
  on lines 2900..2901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2900-2901)
[Warning][Deadcode] Function 'xstrtou_range_sfx' has dead code:
  on line 2937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2937-2937)
  on lines 2942..2944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2942-2944)
  on line 2946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2946-2946)
  on line 2948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2948-2948)
  on line 2971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2971-2971)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 340
  dead: 163 (42 in uncalled functions)
  total lines: 503
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___4 < sizeof(uts->domainname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3004:6-3004:54)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___4 < sizeof(uts->domainname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3004:6-3004:54)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___4 < sizeof(uts->domainname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3004:6-3004:54)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___4 < sizeof(uts->domainname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3004:6-3004:54)
[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/uname-1.i:2898:6-2898:24)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___4 < sizeof(uts->domainname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3004:6-3004:54)
[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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111:27)
[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/uname-1.i:2936:12-2936:62)
[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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111: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/uname-1.i:3111:8-3111:27)
[Warning][Deadcode][CWE-570] condition '! ((6 & spec_flgs) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2698:6-2698:29)
[Warning][Deadcode][CWE-570] condition '(int )first_char == 33' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2425:6-2425:34)
[Warning][Deadcode][CWE-570] condition '(int )*s == 43' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2429:6-2429:26)
[Warning][Deadcode][CWE-571] condition '(flags & requires) == 0u' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2768:7-2768:30)
[Warning][Deadcode][CWE-570] condition '(int )*s == 45' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2432:5-2432:94)
[Warning][Deadcode][CWE-571] condition 'requires == 0u' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2770:8-2770:22)
[Warning][Deadcode][CWE-570] condition 'max_arg >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2778:8-2778:20)
[Warning][Deadcode][CWE-571] condition 'r >= lower' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2956:14-2956:24)
[Warning][Deadcode][CWE-570] condition '! ((int )tmp_if_expr$1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2433:6-2433:34)
[Warning][Deadcode][CWE-571] condition '! ((int )first_char == 33)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2796:6-2796:37)
[Warning][Deadcode][CWE-570] condition '(int )*s == 58' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2442:8-2442:28)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i < sizeof(uts->sysname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2989:6-2989:51)
[Warning][Deadcode][CWE-571] condition '(int const   )*(optstring + opt_index) != 58' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3029:3-3029:84)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i < sizeof(uts->sysname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2989:6-2989:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i < sizeof(uts->sysname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2989:6-2989:51)
[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/uname-1.i:2521:9-2521:17)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i < sizeof(uts->sysname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2989:6-2989:51)
[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/uname-1.i:2523:8-2523:52)
[Warning][Deadcode][CWE-570] condition '(int const   )*(optstring + (opt_index + 1UL)) == 58' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3036:6-3036:68)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i < sizeof(uts->sysname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2989:6-2989:51)
[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/uname-1.i:2527:8-2527:33)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i < sizeof(uts->sysname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2989:6-2989:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i < sizeof(uts->sysname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2989:6-2989:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i < sizeof(uts->sysname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2989:6-2989:51)
[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/uname-1.i:3069:6-3069:41)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___0 < sizeof(uts->nodename) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2992:6-2992:52)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___0 < sizeof(uts->nodename) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2992:6-2992:52)
[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/uname-1.i:3069:6-3069:41)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___0 < sizeof(uts->nodename) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2992:6-2992:52)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___0 < sizeof(uts->nodename) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2992:6-2992:52)
[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/uname-1.i:3069:6-3069:41)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___0 < sizeof(uts->nodename) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2992:6-2992:52)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___0 < sizeof(uts->nodename) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2992:6-2992:52)
[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/uname-1.i:3069:6-3069:41)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___0 < sizeof(uts->nodename) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2992:6-2992:52)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___0 < sizeof(uts->nodename) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2992:6-2992:52)
[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/uname-1.i:3069:6-3069: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/uname-1.i:3069:6-3069:41)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___1 < sizeof(uts->release) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2995:6-2995:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___1 < sizeof(uts->release) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2995:6-2995:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___1 < sizeof(uts->release) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2995:6-2995:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___1 < sizeof(uts->release) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2995:6-2995:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___1 < sizeof(uts->release) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2995:6-2995:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___1 < sizeof(uts->release) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2995:6-2995:51)
[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/uname-1.i:3076:9-3076:29)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___1 < sizeof(uts->release) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2995:6-2995:51)
[Warning][Deadcode][CWE-570] condition '(int )logmode == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2292:6-2292:30)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___1 < sizeof(uts->release) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2995:6-2995:51)
[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/uname-1.i:2294:6-2294:38)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )strerr == (unsigned long )((char const   *)((void *)0)))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2304:6-2304:46)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___2 < sizeof(uts->version) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2998:6-2998:51)
[Warning][Deadcode][CWE-571] condition '! ((unsigned long )applet_long_options == (unsigned long )((char const   *)((void *)0)))' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2457:6-2457:59)
[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/uname-1.i:2321:6-2321:35)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___2 < sizeof(uts->version) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2998:6-2998:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___2 < sizeof(uts->version) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2998:6-2998:51)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )strerr == (unsigned long )((char const   *)((void *)0)))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2336:8-2336:48)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___2 < sizeof(uts->version) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2998:6-2998:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___2 < sizeof(uts->version) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2998:6-2998:51)
[Warning][Deadcode][CWE-571] condition '! ((1 & (int )logmode) == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2353:6-2353:39)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___2 < sizeof(uts->version) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2998:6-2998:51)
[Warning][Deadcode][CWE-570] condition '! ((2 & (int )logmode) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2358:6-2358:39)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___2 < sizeof(uts->version) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2998:6-2998:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___2 < sizeof(uts->version) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2998:6-2998:51)
[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/uname-1.i:2852:9-2852: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/uname-1.i:2757:9-2757: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/uname-1.i:2852:9-2852:17)
[Warning][Deadcode][CWE-570] condition '! (total == 0l)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2390:10-2390:24)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___3 < sizeof(uts->machine) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3001:6-3001:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___3 < sizeof(uts->machine) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3001:6-3001:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___3 < sizeof(uts->machine) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3001:6-3001:51)
[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/uname-1.i:2852:9-2852:17)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___3 < sizeof(uts->machine) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3001:6-3001:51)
[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/uname-1.i:3096:6-3096: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/uname-1.i:2493:11-2493:20)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___3 < sizeof(uts->machine) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3001:6-3001:51)
[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/uname-1.i:3096:6-3096: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/uname-1.i:2852:9-2852:17)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___3 < sizeof(uts->machine) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3001:6-3001:51)
[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/uname-1.i:3096:6-3096:25)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___3 < sizeof(uts->machine) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3001:6-3001:51)
[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/uname-1.i:3096:6-3096: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/uname-1.i:2493:11-2493:20)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___3 < sizeof(uts->machine) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3001:6-3001:51)
[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/uname-1.i:3096:6-3096: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/uname-1.i:2852:9-2852:17)
[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/uname-1.i:3096:6-3096: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/uname-1.i:3096:6-3096: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/uname-1.i:2493:11-2493:20)
[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/uname-1.i:3096:6-3096: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/uname-1.i:2852:9-2852:17)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___4 < sizeof(uts->domainname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3004:6-3004:54)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___4 < sizeof(uts->domainname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3004:6-3004:54)
[Warning][Deadcode][CWE-571] condition '(unsigned long )l_o->flag == (unsigned long )((int *)((void *)0))' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:2497:10-2497:50)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___4 < sizeof(uts->domainname) - 1UL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/uname-1.i:3004:6-3004:54)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
