./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/who-2.i


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2572:3-2583:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2605:3-2606:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2632:7-2638:22 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2622:3-2641:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2650:5-2656:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2663:5-2680:20 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2687:9-2690:9 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2682:5-2700:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2772:13-2775:13 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2860:25-2866:23 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2839:19-2868:19 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2708:3-2882:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2888:5-2907:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2917:5-2920:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2910:3-2944:18 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2946:3-2955:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3004:3-3005:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3025:3-3033:35 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3060:3-3106:18 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3176:11-3190:11 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3235:3-3236:53 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3237:3-3238:53 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3289:3-3290:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3296:3-3302:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3316:3-3317:34 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3331:5-3332:42 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3326:3-3333:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3335:3-3336:23 with factor 2
[Info] longjmp -> enabling longjmp analyses "activeLongjmp, activeSetjmp, taintPartialContexts, modifiedSinceSetjmp, poisonVariables, expsplit, vla"
[Info] Setting "ana.int.interval" to true
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3323:8-3323:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3323:8-3323:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3323:8-3323:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3324:8-3324:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3324:8-3324:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3324:8-3324:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3332:7-3332:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3332:7-3332:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3332:7-3332:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2605:6-2605:82)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2631:7-2631:68)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2631:7-2631:68)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2627:5-2627:47)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2631:7-2631:68)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2459:3-2459:49)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2496:3-2496:29)
[Info][Unsound] Unknown address in {&msg} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2496:3-2496:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2496:3-2496:29)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2501:3-2501:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2501:3-2501: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/who-2.i:2516:3-2516:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2516:3-2516:116)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2516:3-2516:116)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2516:3-2516:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2532:5-2532:29)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2534:5-2534:54)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2535:5-2535:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2551:5-2551:29)
[Info][Imprecise] Invalidating expressions: (struct _IO_FILE *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2565:3-2565:63)
[Info][Imprecise] Invalidating expressions: & return_value_fflush$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2565:3-2565:63)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2556:5-2556:62)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2556:5-2556:62)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2574:5-2574:32)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3027:5-3027:28)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3027:5-3027:28)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3027:5-3027:28)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2572:6-2572:58)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))[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/who-2.i:2574:5-2574:32)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))[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/who-2.i:3027:5-3027:28)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))[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/who-2.i:3027:5-3027:28)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))[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/who-2.i:3027:5-3027:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2581:5-2581:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2572:6-2572:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2581:5-2581:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2572:6-2572:58)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))[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/who-2.i:2574:5-2574:32)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))[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/who-2.i:3027:5-3027:28)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))[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/who-2.i:3027:5-3027:28)
[Info][Unsound] Unknown value in {&(alloc@sid:52(#0))[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/who-2.i:3027:5-3027:28)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___5) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2833:21-2833:84)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___5) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2833:21-2833:84)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___5) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2833:21-2833:84)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2890:10-2890:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2892:12-2892:41)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2898:11-2898:89)
[Info][Unsound] Unknown value in {&(alloc@sid:2112(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2902:11-2902:22)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2890:10-2890:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2892:12-2892:41)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2898:11-2898:89)
[Info][Unsound] Unknown value in {&(alloc@sid:2112)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2902:11-2902:22)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2890:10-2890:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2892:12-2892:41)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2898:11-2898:89)
[Info][Unsound] Unknown value in {&(alloc@sid:2112)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2902:11-2902:22)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2912:5-2912:84)
[Info][Unsound] Unknown value in {&(alloc@sid:2112)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2912:5-2912:84)
[Info][Unsound] Unknown value in {&(alloc@sid:2112(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2912:5-2912:84)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3273:10-3273:39)
[Info][Unsound] Unknown value in {&(alloc@sid:2112)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3273:10-3273:39)
[Info][Unsound] Unknown value in {&(alloc@sid:2112(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3273:10-3273:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3246:6-3246:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3254:7-3254:15)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3256:6-3256:68)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3261:7-3261:15)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2927:7-2927:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2927:7-2927:46)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2931:9-2931:76)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3004:6-3004:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3004:6-3004:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3004:6-3004:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3004:6-3004:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3004:6-3004:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3004:6-3004:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3008:3-3008:56)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3009:4-3009:36)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2936:11-2936:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3114:3-3114:92)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3120:3-3120:114)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3150:6-3150:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3153:5-3153:99)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3160:19-3160:73)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3160:19-3160:73)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3169:5-3169:35)
[Info][Unsound] Unknown address in {&e} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3169:5-3169:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3169:5-3169:35)
[Info][Imprecise] Invalidating expressions: (char ** __restrict  )end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2476:3-2476:25)
[Info][Imprecise] Invalidating expressions: & v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2476:3-2476:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3191:12-3191:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3202:11-3202:141)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3209:3-3209:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2937:11-2937:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2941:13-2941:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2912:5-2912:84)
[Info][Unsound] Unknown value in {&(alloc@sid:2112)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2912:5-2912:84)
[Info][Unsound] Unknown value in {&(alloc@sid:2112(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2912:5-2912:84)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2927:7-2927:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2927:7-2927:46)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2931:9-2931:76)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2936:11-2936:64)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2937:11-2937:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2941:13-2941:48)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2927:7-2927:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2927:7-2927:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2941:13-2941:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2936:11-2936:64)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2937:11-2937:91)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2931:9-2931:76)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2912:5-2912:84)
[Info][Unsound] Unknown value in {&(alloc@sid:2112)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2912:5-2912:84)
[Info][Unsound] Unknown value in {&(alloc@sid:2112(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2912:5-2912:84)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2964:5-2964:25)
[Warning][Unknown] lval (& ut)->ut_line points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3015:3-3015:20)
[Warning][Unknown] lval (& ut)->ut_line points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3016:3-3016:39)
[Warning][Unknown] lval (& ut)->ut_line points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3018:3-3018:49)
[Warning][Unknown] lval (& ut)->ut_line points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3019:10-3019:32)
[Info][Imprecise] Invalidating expressions: (long *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2990:3-2990:59)
[Info][Imprecise] Invalidating expressions: & return_value_time$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2990:3-2990:59)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2991:3-2991:30)
[Info][Imprecise] Invalidating expressions: (char * __restrict  )str6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2996:7-2996:149)
[Info][Imprecise] Invalidating expressions: & return_value_ctime$3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3095:11-3095:47)
[Info][Imprecise] Invalidating expressions: & return_value_ctime$3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3095:11-3095:47)
[Info][Imprecise] Invalidating expressions: & return_value_ctime$3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3095:11-3095:47)
[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/who-2.i:3336:5-3336: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/who-2.i:3336:5-3336: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/who-2.i:3336:5-3336:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:22:1-22:169)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:989:1-993:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:994:1-998:1)
[Warning][Deadcode] Function 'bb_putchar' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2463:1-2468:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3044:1-3046:1)
[Warning][Deadcode] Function 'xfunc_die' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3123:1-3132:1)
[Warning][Deadcode] Function 'sleep' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3224:1-3228:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3275:1-3283:1)
[Warning][Deadcode] Function '__main' has dead code:
  on lines 3100..3101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3100-3101)
  on line 3108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3108-3108)
[Warning][Deadcode] Function 'bb_verror_msg' has dead code:
  on line 2493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2493-2493)
  on line 2495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2495-2495)
  on lines 2506..2507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2506-2507)
  on lines 2523..2526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2523-2526)
  on line 2538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2538-2538)
  on lines 2540..2545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2540-2545)
  on lines 2547..2548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2547-2548)
  on line 2559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2559-2559)
[Warning][Deadcode] Function 'getopt32' has dead code:
  on lines 2648..2650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2648-2650)
  on lines 2653..2655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2653-2655)
  on lines 2658..2662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2658-2662)
  on lines 2665..2666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2665-2666)
  on line 2668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2668-2668)
  on lines 2670..2678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2670-2678)
  on lines 2680..2682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2680-2682)
  on line 2684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2684-2684)
  on lines 2686..2688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2686-2688)
  on line 2690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2690-2690)
  on lines 2692..2696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2692-2696)
  on line 2701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2701-2701)
  on line 2713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2713-2713)
[Warning][Deadcode] Function 'safe_strncpy' has dead code:
  on line 3014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3014-3014)
[Warning][Deadcode] Function 'xmalloc' has dead code:
  on lines 3139..3140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3139-3140)
[Warning][Deadcode] Function 'xstrtou_range_sfx' has dead code:
  on line 3176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3176-3176)
  on lines 3181..3183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3181-3183)
  on line 3185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3185-3185)
  on line 3187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3187-3187)
  on line 3210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3210-3210)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 411
  dead: 89 (20 in uncalled functions)
  total lines: 500
[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/who-2.i:3331:8-3331: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/who-2.i:3331:8-3331: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/who-2.i:2638:13-2638: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/who-2.i:3331:8-3331:27)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___0 < sizeof(dummy_utmp.ut_user)' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3237:7-3237:54)
[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/who-2.i:2638:13-2638: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/who-2.i:3331:8-3331:27)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i___0 < sizeof(dummy_utmp.ut_user)' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3237:7-3237: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/who-2.i:3331:8-3331: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/who-2.i:2638:13-2638: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/who-2.i:3331:8-3331:27)
[Warning][Deadcode][CWE-570] condition 'c >= 32' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2624:8-2624:15)
[Warning][Deadcode][CWE-570] condition 'j < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3331:8-3331: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/who-2.i:2944:9-2944: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/who-2.i:2839:25-2839: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/who-2.i:2638:13-2638: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/who-2.i:2638:13-2638: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/who-2.i:2638:13-2638: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/who-2.i:2638:13-2638: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/who-2.i:2638:13-2638: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/who-2.i:2839:25-2839:33)
[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/who-2.i:3289:6-3289: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/who-2.i:2638:13-2638:22)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )applet_long_options == (unsigned long )((char const   *)((void *)0)))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2644:6-2644:59)
[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/who-2.i:3289:6-3289: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/who-2.i:2839:25-2839:33)
[Warning][Deadcode][CWE-570] condition 'size == 0ul' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3013:6-3013:17)
[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/who-2.i:3296:9-3296:29)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2708:9-2708:17)
[Warning][Deadcode][CWE-571] condition '! ((unsigned long )s == (unsigned long )((unsigned char const   *)((void *)0)))' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2710:8-2710: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/who-2.i:2839:25-2839:33)
[Warning][Deadcode][CWE-570] condition 'do_users != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3054:3-3054:48)
[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/who-2.i:3316:6-3316: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/who-2.i:3316:6-3316: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/who-2.i:3316:6-3316:25)
[Warning][Deadcode][CWE-571] condition 'do_users == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3075:12-3075: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/who-2.i:3316:6-3316: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/who-2.i:3316:6-3316: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/who-2.i:3316:6-3316: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/who-2.i:2839:25-2839:33)
[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/who-2.i:3316:6-3316: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/who-2.i:3106:9-3106:18)
[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/who-2.i:3316:6-3316: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/who-2.i:3316:6-3316: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/who-2.i:3316:6-3316:25)
[Warning][Deadcode][CWE-571] condition 'do_users == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3075:12-3075:25)
[Warning][Deadcode][CWE-570] condition 'i < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3316:6-3316: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/who-2.i:3106:9-3106: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/who-2.i:2839:25-2839:33)
[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/who-2.i:3331:8-3331:27)
[Warning][Deadcode][CWE-571] condition 'do_users == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3075:12-3075:25)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3331:8-3331: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/who-2.i:3331:8-3331: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/who-2.i:3331:8-3331:27)
[Warning][Deadcode][CWE-570] condition '(int )logmode == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2492:6-2492: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/who-2.i:2494:6-2494:38)
[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/who-2.i:3331:8-3331: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/who-2.i:3106:9-3106:18)
[Warning][Deadcode][CWE-570] condition '! (do_users == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3107:6-3107: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/who-2.i:3331:8-3331:27)
[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/who-2.i:2504:6-2504:46)
[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/who-2.i:3331:8-3331: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/who-2.i:3331:8-3331:27)
[Warning][Deadcode][CWE-570] condition '(unsigned long )msg1 == (unsigned long )((char *)((void *)0))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2521:6-2521:35)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2708:9-2708:17)
[Warning][Deadcode][CWE-571] condition '! ((unsigned long )s == (unsigned long )((unsigned char const   *)((void *)0)))' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2710:8-2710:52)
[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/who-2.i:3331:8-3331: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/who-2.i:2839:25-2839:33)
[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/who-2.i:3137:6-3137: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/who-2.i:3331:8-3331:27)
[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/who-2.i:2536:8-2536:48)
[Warning][Deadcode][CWE-570] condition 'j < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3331:8-3331:27)
[Warning][Deadcode][CWE-571] condition '! ((1 & (int )logmode) == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2553:6-2553:39)
[Warning][Deadcode][CWE-570] condition '! ((2 & (int )logmode) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2558:6-2558: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/who-2.i:3331:8-3331: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/who-2.i:3331:8-3331:27)
[Warning][Deadcode][CWE-570] condition '! (total == 0l)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2577:10-2577: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/who-2.i:3331:8-3331: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/who-2.i:3175:12-3175: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/who-2.i:3331:8-3331: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/who-2.i:3331:8-3331: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/who-2.i:3331:8-3331: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/who-2.i:2839:25-2839: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/who-2.i:2944:9-2944: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/who-2.i:3331:8-3331: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/who-2.i:3331:8-3331: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/who-2.i:3331:8-3331: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/who-2.i:3331:8-3331:27)
[Warning][Deadcode][CWE-570] condition 'j < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3331:8-3331:27)
[Warning][Deadcode][CWE-571] condition 'r >= lower' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3195:14-3195: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/who-2.i:3331:8-3331: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/who-2.i:3331:8-3331: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/who-2.i:2944:9-2944: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/who-2.i:3331:8-3331: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/who-2.i:2839:25-2839:33)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i < sizeof(dummy_utmp.ut_line)' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3235:7-3235: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/who-2.i:3331:8-3331:27)
[Warning][Deadcode][CWE-570] condition 'c >= 32' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2624:8-2624:15)
[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/who-2.i:2708:9-2708:17)
[Warning][Deadcode][CWE-571] condition '(unsigned long )i < sizeof(dummy_utmp.ut_line)' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:3235:7-3235:54)
[Warning][Deadcode][CWE-571] condition '! ((unsigned long )s == (unsigned long )((unsigned char const   *)((void *)0)))' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/who-2.i:2710:8-2710:52)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
